let P, Q be pcs; :: thesis: ( P misses Q implies the InternalRel of (pcs-sum P,Q) is transitive )
assume A1: the carrier of P misses the carrier of Q ; :: according to TSEP_1:def 3 :: thesis: the InternalRel of (pcs-sum P,Q) is transitive
pcs-sum P,Q = H₁(P,Q) by Th15;
hence the InternalRel of (pcs-sum P,Q) is transitive by A1, Th1; :: thesis: verum