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;
now :: thesis: for i being Element of NAT holds (SAT M) . [(0 + i),('X' A)] = 1
let 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;
hence M |=0 'G' ('X' A) by LTLAXIO1:10; :: thesis: verum