for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st ( A in LTL0_axioms or A in F ) holds
F |-0 A