let A be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF st F |=0 'G' A holds

F |=0 'G' ('X' A)

let F be Subset of LTLB_WFF; :: thesis: ( F |=0 'G' A implies F |=0 'G' ('X' A) )

assume A1: F |=0 'G' A ; :: thesis: F |=0 'G' ('X' A)

let M be LTLModel; :: according to LTLAXIO5:def 3 :: thesis: ( M |=0 F implies M |=0 'G' ('X' A) )

assume M |=0 F ; :: thesis: M |=0 'G' ('X' A)

then A3: M |=0 'G' A by A1;

F |=0 'G' ('X' A)

let F be Subset of LTLB_WFF; :: thesis: ( F |=0 'G' A implies F |=0 'G' ('X' A) )

assume A1: F |=0 'G' A ; :: thesis: F |=0 'G' ('X' A)

let M be LTLModel; :: according to LTLAXIO5:def 3 :: thesis: ( M |=0 F implies M |=0 'G' ('X' A) )

assume M |=0 F ; :: thesis: M |=0 'G' ('X' A)

then A3: M |=0 'G' A by A1;

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

hence
M |=0 'G' ('X' A)
by LTLAXIO1:10; :: thesis: verumlet i be Element of NAT ; :: thesis: (SAT M) . [(0 + i),('X' A)] = 1

(SAT M) . [(0 + (i + 1)),A] = 1 by LTLAXIO1:10, A3;

hence (SAT M) . [(0 + i),('X' A)] = 1 by LTLAXIO1:9; :: thesis: verum

end;(SAT M) . [(0 + (i + 1)),A] = 1 by LTLAXIO1:10, A3;

hence (SAT M) . [(0 + i),('X' A)] = 1 by LTLAXIO1:9; :: thesis: verum