:: deftheorem defines rng LTLAXIO3:def 8 :
for P being PNPair holds rng P = (rng (P `1)) \/ (rng (P `2));