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