theorem th42: :: PL_AXIOM:53

for p being Element of PL-WFF
for F being Subset of PL-WFF st ( p in PL_axioms or p in F ) holds
F |- p