let P, Q be pcs; :: thesis: ( P misses Q implies pcs-sum P,Q is pcs )
assume A1: P misses Q ; :: thesis: pcs-sum P,Q is pcs
set R = pcs-sum P,Q;
pcs-sum P,Q is pcs-like

proof

A2: field the InternalRel of (pcs-sum P,Q) = the carrier of (pcs-sum P,Q) by ORDERS_1:97;
thus pcs-sum P,Q is reflexive ; :: according to PCS_0:def 23 :: thesis: ( pcs-sum P,Q is transitive & pcs-sum P,Q is pcs-tol-reflexive & pcs-sum P,Q is pcs-tol-symmetric & pcs-sum P,Q is pcs-compatible )
thus pcs-sum P,Q is transitive :: thesis: ( pcs-sum P,Q is pcs-tol-reflexive & pcs-sum P,Q is pcs-tol-symmetric & pcs-sum P,Q is pcs-compatible )

proof

the InternalRel of (pcs-sum P,Q) is transitive by A1, Th18;
hence the InternalRel of (pcs-sum P,Q) is_transitive_in the carrier of (pcs-sum P,Q) by A2, RELAT_2:def 16; :: according to ORDERS_2:def 5 :: thesis: verum

end;

thus ( pcs-sum P,Q is pcs-tol-reflexive & pcs-sum P,Q is pcs-tol-symmetric ) ; :: thesis: pcs-sum P,Q is pcs-compatible
thus pcs-sum P,Q is pcs-compatible by A1, Th19; :: thesis: verum

end;

hence pcs-sum P,Q is pcs ; :: thesis: verum