theorem th15: :: LTLAXIO5:42

for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st A in LTL_axioms holds
F |-0 A