theorem Th16: :: LTLAXIO1:16

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