theorem :: LTLAXIO1:13

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