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:12;
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;
then A3: pcs-sum (P,Q) is transitive ;
pcs-sum (P,Q) is pcs-compatible by A1, Th19;
hence pcs-sum (P,Q) is pcs by A3; :: thesis: verum