theorem Th25: :: LTLAXIO4:25

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