theorem Th8: :: LTLAXIO4:8

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