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)
proof
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;
not {(prop i)} |=0 'X' (prop i) by th262ac1;
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