let P be non empty pcs-Str ; :: thesis: for p, q being Element of
for p', q' being Element of st p = p' & q = q' & not p' (--) q' holds
p (--) q
let p, q be Element of ; :: thesis: for p', q' being Element of st p = p' & q = q' & not p' (--) q' holds
p (--) q
set R = pcs-reverse P;
let p', q' be Element of ; :: thesis: ( p = p' & q = q' & not p' (--) q' implies p (--) q )
assume that
A1: p = p' and
A2: q = q' ; :: thesis: ( p' (--) q' or p (--) q )
A3: the ToleranceRel of (pcs-reverse P) = the ToleranceRel of P ` by Def40;
assume A4: not [p',q'] in the ToleranceRel of (pcs-reverse P) ; :: according to PCS_0:def 7 :: thesis: p (--) q
[p,q] in [:the carrier of P,the carrier of P:] by ZFMISC_1:106;
hence [p,q] in the ToleranceRel of P by A1, A2, A3, A4, XBOOLE_0:def 5; :: according to PCS_0:def 7 :: thesis: verum