theorem Th17: :: LTLAXIO1:17

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