:: deftheorem Def1 defines varcl ABCMIZ_1:def 1 :
for A, b₂ being set holds
( b₂ = varcl A iff ( A c= b₂ & ( for x, y being set st [x,y] in b₂ holds
x c= b₂ ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b₂ c= B ) ) );