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 set ; :: 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:128;
q in the carrier of (pcs-extension P,a) by A5, ZFMISC_1:128;
then [q,p] in [:the carrier of (pcs-extension P,a),{a}:] by A6, ZFMISC_1:129;
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:129;
p in the carrier of (pcs-extension P,a) by A7, ZFMISC_1:129;
then [q,p] in [:{a},the carrier of (pcs-extension P,a):] by A8, ZFMISC_1:128;
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:106;
q in the carrier of P by A9, ZFMISC_1:106;
then [q,p] in the ToleranceRel of P by A3, A9, A10, RELAT_2:def 3;
hence [^,^] in the ToleranceRel of (pcs-extension P,a) by A1, XBOOLE_0:def 3; :: thesis: verum

end;

end;