let n be Nat; :: thesis: for p being Element of Permutations n holds p " is Element of
let p be Element of Permutations n; :: thesis: p " is Element of
reconsider p = p as Permutation of Seg n by Def11;
p " is Element of Permutations n by Def11;
hence p " is Element of by Def13; :: thesis: verum