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;
A2: field the InternalRel of (pcs-sum P,Q) = the carrier of (pcs-sum P,Q) by ORDERS_1:97;
the InternalRel of (pcs-sum P,Q) is transitive by A1, Th18;
then the InternalRel of (pcs-sum P,Q) is_transitive_in the carrier of (pcs-sum P,Q) by A2, RELAT_2:def 16;
then A3: pcs-sum P,Q is transitive by ORDERS_2:def 5;
pcs-sum P,Q is pcs-compatible by A1, Th19;
hence pcs-sum P,Q is pcs by A3; :: thesis: verum