theorem Th6: :: LTLAXIO1:6

for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,TVERUM] = 1