:: deftheorem defines the_subsets_of_card GROUP_10:def 3 :
for E, n being set holds the_subsets_of_card (n,E) = { X where X is Subset of E : card X = n } ;