theorem Th18: :: PCS_0:18
for P, Q being pcs st P misses Q holds
the InternalRel of (pcs-sum (P,Q)) is transitive