theorem Th3: :: ORDINAL5:3

for S1, S2 being Sequence holds
( rng S1 c= rng (S1 ^ S2) & rng S2 c= rng (S1 ^ S2) )