theorem Th9: :: LTLAXIO4:9

for P being PNPair holds rng P c= union (Subt (rng P))