theorem Th18: :: MATRIX_7:18

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