:: deftheorem defines untn LTLAXIO4:def 9 :
for P being PNPair holds untn P = { Q where Q is PNPair : ( rng (Q `1) = untn (rng (P `1)) & rng (Q `2) = untn (rng (P `2)) ) } ;