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 ; :: according to RELAT_2:def 3,PCS_0:def 11 :: thesis: ( 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)) ; :: thesis: [^,^] 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}:] ; :: thesis: [^,^] 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)):] ; :: thesis: [^,^] 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; :: thesis: verum

end;

suppose A7: [p,q] in [: the carrier of (pcs-extension (P,a)),{a}:] ; :: thesis: [^,^] 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; :: thesis: verum

end;

end;

end;

suppose A9: [p,q] in the ToleranceRel of P ; :: thesis: [^,^] in the ToleranceRel of (pcs-extension (P,a))

then A10: p in the carrier of P by ZFMISC_1:87;
q in the carrier of P by A9, ZFMISC_1:87;
then [q,p] in the ToleranceRel of P by A3, A9, A10;
hence [^,^] in the ToleranceRel of (pcs-extension (P,a)) by A1, XBOOLE_0:def 3; :: thesis: verum

end;

end;