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 )

( 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 Z2:
M |=0 'G' A
; :: thesis: M |= Aassume
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;then for i being Element of NAT holds (SAT M) . [(0 + i),A] = 1 ;

hence M |=0 'G' A by LTLAXIO1:10; :: thesis: verum

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

hence
M |= A
; :: thesis: verumlet 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;(SAT M) . [(0 + i),A] = 1 by LTLAXIO1:10, Z2;

hence (SAT M) . [i,A] = 1 ; :: thesis: verum