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

proof

assume A2: [p,q] in the ToleranceRel of (pcs-sum P,Q) ; :: according to PCS_0:def 7 :: thesis: ( ex p', q' being Element of P st
( p' = p & q' = q & p' (--) q' ) or ex p', q' being Element of Q st
( p' = p & q' = q & p' (--) q' ) )

per cases ( [p,q] in the ToleranceRel of P or [p,q] in the ToleranceRel of Q ) by A1, A2, XBOOLE_0:def 3;

suppose A3: [p,q] in the ToleranceRel of P ; :: thesis: ( ex p', q' being Element of P st
( p' = p & q' = q & p' (--) q' ) or ex p', q' being Element of Q st
( p' = p & q' = q & p' (--) q' ) )

then reconsider p' = p, q' = q as Element of P by ZFMISC_1:106;
p' (--) q' by A3, Def7;
hence ( ex p', q' being Element of P st
( p' = p & q' = q & p' (--) q' ) or ex p', q' being Element of Q st
( p' = p & q' = q & p' (--) q' ) ) ; :: thesis: verum

end;

suppose A4: [p,q] in the ToleranceRel of Q ; :: thesis: ( ex p', q' being Element of P st
( p' = p & q' = q & p' (--) q' ) or ex p', q' being Element of Q st
( p' = p & q' = q & p' (--) q' ) )

then reconsider p' = p, q' = q as Element of Q by ZFMISC_1:106;
p' (--) q' by A4, Def7;
hence ( ex p', q' being Element of P st
( p' = p & q' = q & p' (--) q' ) or ex p', q' being Element of Q st
( p' = p & q' = q & p' (--) q' ) ) ; :: thesis: verum

end;

end;

end;

assume A5: ( ex p', q' being Element of P st
( p' = p & q' = q & p' (--) q' ) or ex p', q' being Element of Q st
( p' = p & q' = q & p' (--) q' ) ) ; :: thesis: p (--) q

per cases ( ex p', q' being Element of P st
( p' = p & q' = q & p' (--) q' ) or ex p', q' being Element of Q st
( p' = p & q' = q & p' (--) q' ) ) by A5;

suppose ex p', q' being Element of P st
( p' = p & q' = q & p' (--) q' ) ; :: thesis: p (--) q

then consider p', q' being Element of P such that
A6: ( p' = p & q' = q ) and
A7: p' (--) q' ;
[p',q'] in the ToleranceRel of P by A7, Def7;
hence [p,q] in the ToleranceRel of (pcs-sum P,Q) by A1, A6, XBOOLE_0:def 3; :: according to PCS_0:def 7 :: thesis: verum

end;

suppose ex p', q' being Element of Q st
( p' = p & q' = q & p' (--) q' ) ; :: thesis: p (--) q

then consider p', q' being Element of Q such that
A8: ( p' = p & q' = q ) and
A9: p' (--) q' ;
[p',q'] in the ToleranceRel of Q by A9, Def7;
hence [p,q] in the ToleranceRel of (pcs-sum P,Q) by A1, A8, XBOOLE_0:def 3; :: according to PCS_0:def 7 :: thesis: verum

end;

end;