:: deftheorem Def11 defines CnPos HILBERT1:def 11 :
for X, b₂ being Subset of HP-WFF holds
( b₂ = CnPos X iff for r being Element of HP-WFF holds
( r in b₂ iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) );