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