let P be pcs-Str ; :: thesis:
let a be set ; :: thesis:
let p, q be Element of P; :: thesis:
let p1, q1 be Element of (pcs-extension P,a); :: thesis:
assume that
A1: ( p = p1 & q = q1 ) and
A2: ( p <> a & q <> a ) and
A3: p1 (--) q1 ; :: thesis:
set R = pcs-extension P,a;
A4: 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;
[p1,q1] in the ToleranceRel of (pcs-extension P,a) by A3, Def7;
then ( [p1,q1] in [:{a},the carrier of (pcs-extension P,a):] \/ [:the carrier of (pcs-extension P,a),{a}:] or [p1,q1] in the ToleranceRel of P ) by A4, XBOOLE_0:def 3;
then ( [p1,q1] in [:{a},the carrier of (pcs-extension P,a):] or [p1,q1] in [:the carrier of (pcs-extension P,a),{a}:] or [p1,q1] in the ToleranceRel of P ) by XBOOLE_0:def 3;
hence [p,q] in the ToleranceRel of P by A1, A2, ZFMISC_1:128, ZFMISC_1:129; :: according to PCS_0:def 7 :: thesis: