set R = pcs-extension (P,a);
A1:
the ToleranceRel of (pcs-extension (P,a)) = ([:{a}, the carrier of (pcs-extension (P,a)):] \/ [: the carrier of (pcs-extension (P,a)),{a}:]) \/ the ToleranceRel of P
by Def39;
let p, q be object ; RELAT_2:def 3,PCS_0:def 11 ( not p in the carrier of (pcs-extension (P,a)) or not q in the carrier of (pcs-extension (P,a)) or not [^,^] in the ToleranceRel of (pcs-extension (P,a)) or [^,^] in the ToleranceRel of (pcs-extension (P,a)) )
assume that
p in the carrier of (pcs-extension (P,a))
and
q in the carrier of (pcs-extension (P,a))
and
A2:
[p,q] in the ToleranceRel of (pcs-extension (P,a))
; [^,^] in the ToleranceRel of (pcs-extension (P,a))
A3:
the ToleranceRel of P is_symmetric_in the carrier of P
by Def11;
per cases
( [p,q] in [:{a}, the carrier of (pcs-extension (P,a)):] \/ [: the carrier of (pcs-extension (P,a)),{a}:] or [p,q] in the ToleranceRel of P )
by A1, A2, XBOOLE_0:def 3;
suppose A4:
[p,q] in [:{a}, the carrier of (pcs-extension (P,a)):] \/ [: the carrier of (pcs-extension (P,a)),{a}:]
;
[^,^] in the ToleranceRel of (pcs-extension (P,a))per cases
( [p,q] in [:{a}, the carrier of (pcs-extension (P,a)):] or [p,q] in [: the carrier of (pcs-extension (P,a)),{a}:] )
by A4, XBOOLE_0:def 3;
suppose A5:
[p,q] in [:{a}, the carrier of (pcs-extension (P,a)):]
;
[^,^] in the ToleranceRel of (pcs-extension (P,a))then A6:
p = a
by ZFMISC_1:105;
q in the
carrier of
(pcs-extension (P,a))
by A5, ZFMISC_1:105;
then
[q,p] in [: the carrier of (pcs-extension (P,a)),{a}:]
by A6, ZFMISC_1:106;
then
[q,p] in [:{a}, the carrier of (pcs-extension (P,a)):] \/ [: the carrier of (pcs-extension (P,a)),{a}:]
by XBOOLE_0:def 3;
hence
[^,^] in the
ToleranceRel of
(pcs-extension (P,a))
by A1, XBOOLE_0:def 3;
verum end; suppose A7:
[p,q] in [: the carrier of (pcs-extension (P,a)),{a}:]
;
[^,^] in the ToleranceRel of (pcs-extension (P,a))then A8:
q = a
by ZFMISC_1:106;
p in the
carrier of
(pcs-extension (P,a))
by A7, ZFMISC_1:106;
then
[q,p] in [:{a}, the carrier of (pcs-extension (P,a)):]
by A8, ZFMISC_1:105;
then
[q,p] in [:{a}, the carrier of (pcs-extension (P,a)):] \/ [: the carrier of (pcs-extension (P,a)),{a}:]
by XBOOLE_0:def 3;
hence
[^,^] in the
ToleranceRel of
(pcs-extension (P,a))
by A1, XBOOLE_0:def 3;
verum end;