:: deftheorem Def6 defines PL-WFF PL_AXIOM:def 3 :
for b₁ being set holds
( b₁ = PL-WFF iff ( b₁ is PL-closed & ( for D being set st D is PL-closed holds
b₁ c= D ) ) );