:: deftheorem defplax defines PL_axioms PL_AXIOM:def 20 :
for b₁ being Subset of PL-WFF holds
( b₁ = PL_axioms iff ( b₁ is with_PL_axioms & ( for D being Subset of PL-WFF st D is with_PL_axioms holds
b₁ c= D ) ) );