:: deftheorem Def13 defines ^^ COMBGRAS:def 13 :
for k being Nat
for X being non empty set st 0 < k & k + 1 c= card X holds
for A being finite set st card A = k - 1 holds
^^ (A,X,k) = ^^ (A,X);