:: deftheorem defines ^^ COMBGRAS:def 12 :
for X being set
for A being finite set holds ^^ (A,X) = { B where B is Subset of X : ( card B = (card A) + 1 & A c= B ) } ;