:: deftheorem Def4 defines Universe_closure CLASSES2:def 4 :
for X being set
for b₂ being Universe holds
( b₂ = Universe_closure X iff ( X c= b₂ & ( for Y being Universe st X c= Y holds
b₂ c= Y ) ) );