for X, f being set st f in permutations X holds
f is Permutation of X