:: deftheorem Def8 defines MC-wff INTPRO_1:def 8 :
for b₁ being set holds
( b₁ = MC-wff iff ( b₁ is MC-closed & ( for E being set st E is MC-closed holds
b₁ c= E ) ) );