let A be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF st A in LTL0_axioms holds

F |- A

let F be Subset of LTLB_WFF; :: thesis: ( A in LTL0_axioms implies F |- A )

assume A in LTL0_axioms ; :: thesis: F |- A

then consider B being Element of LTLB_WFF such that

A1: ( A = 'G' B & B in LTL_axioms ) ;

F |- B by A1, LTLAXIO1:42;

hence F |- A by A1, LTLAXIO1:54; :: thesis: verum

F |- A

let F be Subset of LTLB_WFF; :: thesis: ( A in LTL0_axioms implies F |- A )

assume A in LTL0_axioms ; :: thesis: F |- A

then consider B being Element of LTLB_WFF such that

A1: ( A = 'G' B & B in LTL_axioms ) ;

F |- B by A1, LTLAXIO1:42;

hence F |- A by A1, LTLAXIO1:54; :: thesis: verum