let A be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF st F |= A holds
F |= 'G' A
let F be Subset of LTLB_WFF; :: thesis: ( F |= A implies F |= 'G' A )
assume A1: F |= A ; :: thesis: F |= 'G' A
let M be LTLModel; :: according to LTLAXIO1:def 14 :: thesis: ( M |= F implies M |= 'G' A )
assume A2: M |= F ; :: thesis: M |= 'G' A
let n be Element of NAT ; :: according to LTLAXIO1:def 12 :: thesis: (SAT M) . [n,('G' A)] = 1
for i being Element of NAT holds (SAT M) . [(n + i),A] = 1 by Def12, A1, A2;
hence (SAT M) . [n,('G' A)] = 1 by Th10; :: thesis: verum