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