let P, Q be pcs-Str ; :: thesis: 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)); :: thesis: ( 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 InternalRel of (pcs-sum (P,Q)) = the InternalRel of P \/ the InternalRel 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 ) ) :: thesis: ( ( 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 )

proof

assume A2: [p,q] in the InternalRel of (pcs-sum (P,Q)) ; :: according to ORDERS_2:def 5 :: thesis: ( 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 ) )

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

suppose A3: [p,q] in the InternalRel of P ; :: thesis: ( 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 ) )

then reconsider p9 = p, q9 = q as Element of P by ZFMISC_1:87;
p9 <= q9 by A3;
hence ( 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 ) ) ; :: thesis: verum

end;

suppose A4: [p,q] in the InternalRel of Q ; :: thesis: ( 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 ) )

then reconsider p9 = p, q9 = q as Element of Q by ZFMISC_1:87;
p9 <= q9 by A4;
hence ( 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 ) ) ; :: thesis: verum

end;

end;

end;

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 ) ) ; :: thesis: p <= q

per cases ( 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 ) ) by A5;

suppose ex p9, q9 being Element of P st
( p9 = p & q9 = q & p9 <= q9 ) ; :: thesis: p <= q

then consider p9, q9 being Element of P such that
A6: p9 = p and
A7: q9 = q and
A8: p9 <= q9 ;
[p9,q9] in the InternalRel of P by A8;
hence [p,q] in the InternalRel of (pcs-sum (P,Q)) by A1, A6, A7, XBOOLE_0:def 3; :: according to ORDERS_2:def 5 :: thesis: verum

end;

suppose ex p9, q9 being Element of Q st
( p9 = p & q9 = q & p9 <= q9 ) ; :: thesis: p <= q

then consider p9, q9 being Element of Q such that
A9: p9 = p and
A10: q9 = q and
A11: p9 <= q9 ;
[p9,q9] in the InternalRel of Q by A11;
hence [p,q] in the InternalRel of (pcs-sum (P,Q)) by A1, A9, A10, XBOOLE_0:def 3; :: according to ORDERS_2:def 5 :: thesis: verum

end;

end;