:: deftheorem defines rngr LTLAXIO4:def 12 :
for P being PNPair
for T being pnptree of P holds rngr T = { (T . t) where t is Node of T : t <> {} } ;