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 )
hereby :: thesis: ( M |=0 'G' F implies M |= F )
assume Z1: M |= F ; :: thesis: M |=0 'G' F
thus M |=0 'G' F :: thesis: verum
proof
let A be Element of LTLB_WFF ; :: according to LTLAXIO5:def 2 :: thesis: ( A in 'G' F implies M |=0 A )
assume A in 'G' F ; :: thesis: M |=0 A
then consider B being Element of LTLB_WFF such that
A1: ( A = 'G' B & B in F ) ;
thus M |=0 A by A1, th261b, Z1; :: thesis: verum
end;
end;
assume Z1: M |=0 'G' F ; :: thesis: M |= 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