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