let p be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF st F |- p holds

F |- 'G' p

let F be Subset of LTLB_WFF; :: thesis: ( F |- p implies F |- 'G' p )

assume A1: F |- p ; :: thesis: F |- 'G' p

p => (p => p) in LTL_axioms by Th34;

then F |- p => (p => p) by Th42;

then A2: F |- p => p by A1, Th43;

('X' p) => (p => ('X' p)) in LTL_axioms by Th34;

then A3: F |- ('X' p) => (p => ('X' p)) by Th42;

F |- 'X' p by A1, Th44;

then F |- p => ('X' p) by A3, Th43;

then F |- p => ('G' p) by A2, Th45;

hence F |- 'G' p by A1, Th43; :: thesis: verum

F |- 'G' p

let F be Subset of LTLB_WFF; :: thesis: ( F |- p implies F |- 'G' p )

assume A1: F |- p ; :: thesis: F |- 'G' p

p => (p => p) in LTL_axioms by Th34;

then F |- p => (p => p) by Th42;

then A2: F |- p => p by A1, Th43;

('X' p) => (p => ('X' p)) in LTL_axioms by Th34;

then A3: F |- ('X' p) => (p => ('X' p)) by Th42;

F |- 'X' p by A1, Th44;

then F |- p => ('X' p) by A3, Th43;

then F |- p => ('G' p) by A2, Th45;

hence F |- 'G' p by A1, Th43; :: thesis: verum