:: deftheorem Def2 defines ||^ RAMSEY_1:def 2 :
for n being Nat
for X, Y being set
for f being Function of X,Y st f is one-to-one & card n c= card X & not X is empty & not Y is empty holds
f ||^ n = (.: f) | (the_subsets_of_card (n,X));