theorem Th31: :: LTLAXIO4:31

for A, B being Element of LTLB_WFF
for P being consistent complete PNPair
for T being pnptree of P st A 'U' B in rng (P `1) & ( for Q being Element of rngr T holds not B in rng (Q `1) ) holds
for Q being Element of rngr T holds
( B in rng (Q `2) & A 'U' B in rng (Q `1) )