set n = the Nat;
set p = the Permutation of (Seg the Nat);
take P = { the Permutation of (Seg the Nat)}; :: thesis: ( P is permutational & not P is empty )
thus P is permutational :: thesis: not P is empty

proof

take the Nat ; :: according to MATRIX_1:def 10 :: thesis: for x being set st x in P holds
x is Permutation of (Seg the Nat)
let x be set ; :: thesis: ( x in P implies x is Permutation of (Seg the Nat) )
assume x in P ; :: thesis: x is Permutation of (Seg the Nat)
hence x is Permutation of (Seg the Nat) by TARSKI:def 1; :: thesis: verum

end;

thus not P is empty ; :: thesis: verum