let P1, P2 be set ; :: thesis: ( ( for x being set holds

( x in P1 iff x is Permutation of (Seg n) ) ) & ( for x being set holds

( x in P2 iff x is Permutation of (Seg n) ) ) implies P1 = P2 )

assume that

A3: for x being set holds

( x in P1 iff x is Permutation of (Seg n) ) and

A4: for x being set holds

( x in P2 iff x is Permutation of (Seg n) ) ; :: thesis: P1 = P2

( x in P1 iff x is Permutation of (Seg n) ) ) & ( for x being set holds

( x in P2 iff x is Permutation of (Seg n) ) ) implies P1 = P2 )

assume that

A3: for x being set holds

( x in P1 iff x is Permutation of (Seg n) ) and

A4: for x being set holds

( x in P2 iff x is Permutation of (Seg n) ) ; :: thesis: P1 = P2

A5: now :: thesis: for x being object st x in P2 holds

x in P1

x in P1

let x be object ; :: thesis: ( x in P2 implies x in P1 )

assume x in P2 ; :: thesis: x in P1

then x is Permutation of (Seg n) by A4;

hence x in P1 by A3; :: thesis: verum

end;assume x in P2 ; :: thesis: x in P1

then x is Permutation of (Seg n) by A4;

hence x in P1 by A3; :: thesis: verum

now :: thesis: for x being object st x in P1 holds

x in P2

hence
P1 = P2
by A5, TARSKI:2; :: thesis: verumx in P2

let x be object ; :: thesis: ( x in P1 implies x in P2 )

assume x in P1 ; :: thesis: x in P2

then x is Permutation of (Seg n) by A3;

hence x in P2 by A4; :: thesis: verum

end;assume x in P1 ; :: thesis: x in P2

then x is Permutation of (Seg n) by A3;

hence x in P2 by A4; :: thesis: verum