theorem Th24: :: LTLAXIO4:24

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