theorem Th5: :: LTLAXIO4:5

for p, q being Element of LTLB_WFF
for M being LTLModel
for i being Element of NAT holds
( (SAT M) . [i,(p 'U' q)] = 1 iff ex j being Element of NAT st
( j > i & (SAT M) . [j,q] = 1 & ( for k being Element of NAT st i < k & k < j holds
(SAT M) . [k,p] = 1 ) ) )