let A be Element of LTLB_WFF ; :: thesis: for M being LTLModel holds
( M |= A iff M |=0 'G' A )
let M be LTLModel; :: thesis: ( M |= A iff M |=0 'G' A )

hereby :: thesis: ( M |=0 'G' A implies M |= A )

assume M |= A ; :: thesis: M |=0 'G' A
then for i being Element of NAT holds (SAT M) . [(0 + i),A] = 1 ;
hence M |=0 'G' A by LTLAXIO1:10; :: thesis: verum

end;

assume Z2: M |=0 'G' A ; :: thesis: M |= A

now :: thesis: for i being Element of NAT holds (SAT M) . [i,A] = 1

let i be Element of NAT ; :: thesis: (SAT M) . [i,A] = 1
(SAT M) . [(0 + i),A] = 1 by LTLAXIO1:10, Z2;
hence (SAT M) . [i,A] = 1 ; :: thesis: verum

end;

hence M |= A ; :: thesis: verum