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

F |=0 A

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

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

let M be LTLModel; :: according to LTLAXIO5:def 3 :: thesis: ( M |=0 F implies M |=0 A )

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

then M |=0 'G' A by Z1;

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

hence (SAT M) . [0,A] = 1 ; :: according to LTLAXIO5:def 1 :: thesis: verum

F |=0 A

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

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

let M be LTLModel; :: according to LTLAXIO5:def 3 :: thesis: ( M |=0 F implies M |=0 A )

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

then M |=0 'G' A by Z1;

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

hence (SAT M) . [0,A] = 1 ; :: according to LTLAXIO5:def 1 :: thesis: verum