theorem Th22: :: LTLAXIO4:22

for A, B being Element of LTLB_WFF
for P, Q being PNPair st A 'U' B in rng (P `1) & Q in compn P holds
untn (A,B) in rng (Q `1)