theorem Th21: :: LTLAXIO4:21

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