theorem Th30: :: LTLAXIO4:30

for A, B being Element of LTLB_WFF
for i being Nat
for P being consistent complete PNPair
for T being pnptree of P
for t being path of T st A 'U' B in rng ((T . (t . i)) `2) holds
for j being Element of NAT holds
( not j > i or B in rng ((T . (t . j)) `2) or ex k being Element of NAT st
( i < k & k < j & A in rng ((T . (t . k)) `2) ) )