theorem Th32: :: LTLAXIO4:32

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) holds
ex R being Element of rngr T st B in rng (R `1)