theorem Th1: :: PCS_0:1

for R1, S1 being set
for R being transitive Relation of R1
for S being transitive Relation of S1 st R1 misses S1 holds
R \/ S is transitive