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