let P, Q be pcs-Str ; for p, q being Element of (pcs-sum (P,Q)) holds
( p (--) q iff ( ex p9, q9 being Element of P st
( p9 = p & q9 = q & p9 (--) q9 ) or ex p9, q9 being Element of Q st
( p9 = p & q9 = q & p9 (--) q9 ) ) )
set R = pcs-sum (P,Q);
let p, q be Element of (pcs-sum (P,Q)); ( p (--) q iff ( ex p9, q9 being Element of P st
( p9 = p & q9 = q & p9 (--) q9 ) or ex p9, q9 being Element of Q st
( p9 = p & q9 = q & p9 (--) q9 ) ) )
A1:
the ToleranceRel of (pcs-sum (P,Q)) = the ToleranceRel of P \/ the ToleranceRel of Q
by Th14;
thus
( not p (--) q or ex p9, q9 being Element of P st
( p9 = p & q9 = q & p9 (--) q9 ) or ex p9, q9 being Element of Q st
( p9 = p & q9 = q & p9 (--) q9 ) )
( ( ex p9, q9 being Element of P st
( p9 = p & q9 = q & p9 (--) q9 ) or ex p9, q9 being Element of Q st
( p9 = p & q9 = q & p9 (--) q9 ) ) implies p (--) q )
assume A5:
( ex p9, q9 being Element of P st
( p9 = p & q9 = q & p9 (--) q9 ) or ex p9, q9 being Element of Q st
( p9 = p & q9 = q & p9 (--) q9 ) )
; p (--) q