theorem Th2: :: LTLAXIO5:29

for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st A in LTL0_axioms holds
F |=0 A