theorem Th42: :: LTLAXIO1:42

for p being Element of LTLB_WFF
for X being Subset of LTLB_WFF st ( p in LTL_axioms or p in X ) holds
X |- p