theorem Th5: :: LTLAXIO1:5

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