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

proof

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

end;

thus not P is empty ; :: thesis: verum