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