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

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

thus
not P is empty
; :: thesis: verum
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;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