:: deftheorem Def1 defines subset-closed_closure_of SIMPLEX0:def 1 :
for X being set
for b₂ being subset-closed set holds
( b₂ = subset-closed_closure_of X iff ( X c= b₂ & ( for Y being set st X c= Y & Y is subset-closed holds
b₂ c= Y ) ) );