theorem Th27: :: LTLAXIO4:27

for P, Q being PNPair
for T being pnptree of P st Q in rng T holds
rng Q c= union (Subt (rng P))