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