:: deftheorem Def1 defines subset-closed CLASSES1:def 1 :
for B being set holds
( B is subset-closed iff for X, Y being set st X in B & Y c= X holds
Y in B );