theorem Th23: :: LTLAXIO4:23

for P, Q, R being PNPair st R in compn Q & rng Q c= union (Subt (rng P)) holds
rng R c= union (Subt (rng P))