let A be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF st A in LTL_axioms holds
F |-0 A
let F be Subset of LTLB_WFF; :: thesis: ( A in LTL_axioms implies F |-0 A )
assume A in LTL_axioms ; :: thesis: F |-0 A
then 'G' A in LTL0_axioms ;
then F |-0 'G' A by th10;
hence F |-0 A by th9; :: thesis: verum