for n being Nat
for p being Element of Permutations n holds p " is Element of Permutations n