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