:: deftheorem defines permutations CAYLEY:def 1 :
for X being set holds permutations X = { f where f is Permutation of X : verum } ;