:: deftheorem Def2 defines the_subsets_with_limited_card SIMPLEX0:def 2 :
for Y, X, n being set
for b₄ being Subset-Family of Y holds
( b₄ = the_subsets_with_limited_card (n,X,Y) iff for A being Subset of Y holds
( A in b₄ iff ( A in X & card A c= n ) ) );