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

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