let i be Element of NAT ; :: thesis: ( {(prop i)} |= prop i & not {(prop i)} |=0 'G' (prop i) )

thus {(prop i)} |= prop i :: thesis: not {(prop i)} |=0 'G' (prop i)

then consider M being LTLModel such that

A2: ( M |=0 {(prop i)} & not M |=0 'X' (prop i) ) ;

not (SAT M) . [(0 + 1),(prop i)] = 1 by LTLAXIO1:9, A2;

then not M |=0 'G' (prop i) by LTLAXIO1:10;

hence not {(prop i)} |=0 'G' (prop i) by A2; :: thesis: verum

thus {(prop i)} |= prop i :: thesis: not {(prop i)} |=0 'G' (prop i)

proof

not {(prop i)} |=0 'X' (prop i)
by th262ac1;
let M be LTLModel; :: according to LTLAXIO1:def 14 :: thesis: ( not M |= {(prop i)} or M |= prop i )

A1: prop i in {(prop i)} by TARSKI:def 1;

assume M |= {(prop i)} ; :: thesis: M |= prop i

hence M |= prop i by A1; :: thesis: verum

end;A1: prop i in {(prop i)} by TARSKI:def 1;

assume M |= {(prop i)} ; :: thesis: M |= prop i

hence M |= prop i by A1; :: thesis: verum

then consider M being LTLModel such that

A2: ( M |=0 {(prop i)} & not M |=0 'X' (prop i) ) ;

not (SAT M) . [(0 + 1),(prop i)] = 1 by LTLAXIO1:9, A2;

then not M |=0 'G' (prop i) by LTLAXIO1:10;

hence not {(prop i)} |=0 'G' (prop i) by A2; :: thesis: verum