let P be pcs-Str ; for a being set
for p, q being Element of (pcs-extension (P,a)) st p = a holds
( p (--) q & q (--) p )
let a be set ; for p, q being Element of (pcs-extension (P,a)) st p = a holds
( p (--) q & q (--) p )
set R = pcs-extension (P,a);
let p, q be Element of (pcs-extension (P,a)); ( p = a implies ( p (--) q & q (--) p ) )
assume A1:
p = a
; ( p (--) q & q (--) p )
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;
then A2:
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 XBOOLE_1:4;
A3:
[a,q] in [:{a}, the carrier of (pcs-extension (P,a)):]
by ZFMISC_1:105;
[q,a] in [: the carrier of (pcs-extension (P,a)),{a}:]
by ZFMISC_1:106;
then
[q,a] in [: the carrier of (pcs-extension (P,a)),{a}:] \/ the ToleranceRel of P
by XBOOLE_0:def 3;
hence
( [p,q] in the ToleranceRel of (pcs-extension (P,a)) & [q,p] in the ToleranceRel of (pcs-extension (P,a)) )
by A1, A2, A3, XBOOLE_0:def 3; PCS_0:def 7 verum