let F be Subset of LTLB_WFF; :: thesis: for M being LTLModel holds

( M |= F iff M |=0 'G' F )

let M be LTLModel; :: thesis: ( M |= F iff M |=0 'G' F )

let A be Element of LTLB_WFF ; :: according to LTLAXIO1:def 13 :: thesis: ( not A in F or M |= A )

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

then 'G' A in 'G' F ;

hence M |= A by th261b, Z1; :: thesis: verum

( M |= F iff M |=0 'G' F )

let M be LTLModel; :: thesis: ( M |= F iff M |=0 'G' F )

hereby :: thesis: ( M |=0 'G' F implies M |= F )
end;

assume Z1:
M |=0 'G' F
; :: thesis: M |= Flet A be Element of LTLB_WFF ; :: according to LTLAXIO1:def 13 :: thesis: ( not A in F or M |= A )

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

then 'G' A in 'G' F ;

hence M |= A by th261b, Z1; :: thesis: verum