theorem Th12: :: LTLAXIO1:12

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