let P be pcs-Str ; :: thesis: for a being set
for p, q being Element of P
for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 & q = q1 & p <> a & q <> a & p1 (--) q1 holds
p (--) q
let a be set ; :: thesis: for p, q being Element of P
for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 & q = q1 & p <> a & q <> a & p1 (--) q1 holds
p (--) q
let p, q be Element of P; :: thesis: for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 & q = q1 & p <> a & q <> a & p1 (--) q1 holds
p (--) q
let p1, q1 be Element of (pcs-extension (P,a)); :: thesis: ( p = p1 & q = q1 & p <> a & q <> a & p1 (--) q1 implies p (--) q )
assume that
A1: p = p1 and
A2: q = q1 and
A3: p <> a and
A4: q <> a and
A5: p1 (--) q1 ; :: thesis: p (--) q
set R = pcs-extension (P,a);
A6: 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 A5, 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 A6, 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, A3, A4, ZFMISC_1:105, ZFMISC_1:106; :: according to PCS_0:def 7 :: thesis: verum