theorem Th9: :: LTLAXIO1:9

for A being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,('X' A)] = (SAT M) . [(n + 1),A]