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

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