theorem Th18: :: LTLAXIO1:18

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