let A be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF st F |=0 'G' A holds

F |= A

let F be Subset of LTLB_WFF; :: thesis: ( F |=0 'G' A implies F |= A )

assume Z1: F |=0 'G' A ; :: thesis: F |= A

assume not F |= A ; :: thesis: contradiction

then consider M being LTLModel such that

A1: ( M |= F & not M |= A ) ;

A3: M |=0 F

A2: not (SAT M) . [i,A] = 1 by A1;

M |=0 'G' A by A3, Z1;

then (SAT M) . [(0 + i),A] = 1 by LTLAXIO1:10;

hence contradiction by A2; :: thesis: verum

F |= A

let F be Subset of LTLB_WFF; :: thesis: ( F |=0 'G' A implies F |= A )

assume Z1: F |=0 'G' A ; :: thesis: F |= A

assume not F |= A ; :: thesis: contradiction

then consider M being LTLModel such that

A1: ( M |= F & not M |= A ) ;

A3: M |=0 F

proof

consider i being Element of NAT such that
let A be Element of LTLB_WFF ; :: according to LTLAXIO5:def 2 :: thesis: ( A in F implies M |=0 A )

assume A in F ; :: thesis: M |=0 A

then M |= A by A1;

hence M |=0 A ; :: thesis: verum

end;assume A in F ; :: thesis: M |=0 A

then M |= A by A1;

hence M |=0 A ; :: thesis: verum

A2: not (SAT M) . [i,A] = 1 by A1;

M |=0 'G' A by A3, Z1;

then (SAT M) . [(0 + i),A] = 1 by LTLAXIO1:10;

hence contradiction by A2; :: thesis: verum