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:128;
[q,a] in [:the carrier of (pcs-extension P,a),{a}:]
by ZFMISC_1:129;
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