now

let p be set ; :: thesis: ( p in Permutations 3 implies p in {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} )
assume p in Permutations 3 ; :: thesis: p in {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>}
then reconsider q = p as Permutation of (Seg 3) by MATRIX_2:def 11;
A1: ( q is Function of (Seg 3),(Seg 3) & rng q = Seg 3 ) by FUNCT_2:def 3;
A2: dom q = Seg 3 by FUNCT_2:67;
A3: ( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 ) ;
then q . 1 in Seg 3 by A1, FUNCT_2:6;
then A4: ( q . 1 = 1 or q . 1 = 2 or q . 1 = 3 ) by ENUMSET1:def 1, FINSEQ_3:1;
q . 2 in Seg 3 by A1, A3, FUNCT_2:6;
then A5: ( q . 2 = 1 or q . 2 = 2 or q . 2 = 3 ) by ENUMSET1:def 1, FINSEQ_3:1;
q . 3 in Seg 3 by A1, A3, FUNCT_2:6;
then A6: ( q . 3 = 1 or q . 3 = 2 or q . 3 = 3 ) by ENUMSET1:def 1, FINSEQ_3:1;
( ( not ( q . 1 = 1 & q . 2 = 2 & q . 3 = 3 ) & not ( q . 1 = 3 & q . 2 = 2 & q . 3 = 1 ) & not ( q . 1 = 1 & q . 2 = 3 & q . 3 = 2 ) & not ( q . 1 = 2 & q . 2 = 3 & q . 3 = 1 ) & not ( q . 1 = 2 & q . 2 = 1 & q . 3 = 3 ) & not ( q . 1 = 3 & q . 2 = 1 & q . 3 = 2 ) ) or q = <*1,2,3*> or q = <*3,2,1*> or q = <*1,3,2*> or q = <*2,3,1*> or q = <*2,1,3*> or q = <*3,1,2*> )

proof

reconsider q = q as FinSequence by A2, FINSEQ_1:def 2;
len q = 3 by A2, FINSEQ_1:def 3;
hence ( ( not ( q . 1 = 1 & q . 2 = 2 & q . 3 = 3 ) & not ( q . 1 = 3 & q . 2 = 2 & q . 3 = 1 ) & not ( q . 1 = 1 & q . 2 = 3 & q . 3 = 2 ) & not ( q . 1 = 2 & q . 2 = 3 & q . 3 = 1 ) & not ( q . 1 = 2 & q . 2 = 1 & q . 3 = 3 ) & not ( q . 1 = 3 & q . 2 = 1 & q . 3 = 2 ) ) or q = <*1,2,3*> or q = <*3,2,1*> or q = <*1,3,2*> or q = <*2,3,1*> or q = <*2,1,3*> or q = <*3,1,2*> ) by FINSEQ_1:62; :: thesis: verum

end;

then ( p in {<*1,2,3*>,<*3,2,1*>} or q in {<*1,3,2*>,<*2,3,1*>} or q in {<*2,1,3*>,<*3,1,2*>} ) by A2, A3, A4, A5, A6, FUNCT_1:def 8, TARSKI:def 2;
then ( p in {<*1,2,3*>,<*3,2,1*>} or q in {<*1,3,2*>,<*2,3,1*>} \/ {<*2,1,3*>,<*3,1,2*>} ) by XBOOLE_0:def 3;
then ( p in {<*1,2,3*>,<*3,2,1*>} or q in {<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} ) by ENUMSET1:45;
then p in {<*1,2,3*>,<*3,2,1*>} \/ {<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} by XBOOLE_0:def 3;
hence p in {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} by ENUMSET1:52; :: thesis: verum

end;

then A7: Permutations 3 c= {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} implies x in Permutations 3 )
assume x in {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} ; :: thesis: x in Permutations 3
then x in {<*1,2,3*>,<*3,2,1*>} \/ {<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} by ENUMSET1:52;
then ( x in {<*1,2,3*>,<*3,2,1*>} or x in {<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} ) by XBOOLE_0:def 3;
then ( x in {<*1,2,3*>,<*3,2,1*>} or x in {<*1,3,2*>,<*2,3,1*>} \/ {<*2,1,3*>,<*3,1,2*>} ) by ENUMSET1:45;
then A8: ( x in {<*1,2,3*>,<*3,2,1*>} or x in {<*1,3,2*>,<*2,3,1*>} or x in {<*2,1,3*>,<*3,1,2*>} ) by XBOOLE_0:def 3;
A9: idseq 3 in Permutations 3 by MATRIX_2:def 11;
A10: Rev (idseq 3) in Permutations 3 by Th4;
A11: <*1,3,2*> in Permutations 3

proof

reconsider f = <*1,2,3*> as one-to-one FinSequence-like Function of (Seg 3),(Seg 3) by FINSEQ_2:62;
reconsider h = <*2,3*> as FinSequence of NAT ;
A12: f = <*1*> ^ h by FINSEQ_1:60;
Rev h = <*3,2*> by FINSEQ_5:64;
then <*1*> ^ (Rev h) = <*1,3,2*> by FINSEQ_1:60;
hence <*1,3,2*> in Permutations 3 by A9, A12, Th17, FINSEQ_2:62; :: thesis: verum

end;

A13: <*2,3,1*> in Permutations 3

proof

reconsider f = <*1,2,3*> as one-to-one FinSequence-like Function of (Seg 3),(Seg 3) by FINSEQ_2:62;
reconsider h = <*2,3*> as FinSequence of NAT ;
f = <*1*> ^ h by FINSEQ_1:60;
hence <*2,3,1*> in Permutations 3 by A9, Th18, FINSEQ_2:62; :: thesis: verum

end;

A14: <*2,1,3*> in Permutations 3

proof

reconsider h = <*1,2*> as FinSequence of NAT ;
A15: <*3*> ^ h in Permutations 3 by A9, Th18, FINSEQ_2:62;
A16: Rev h = <*2,1*> by FINSEQ_5:64;
<*3*> ^ (Rev h) in Permutations 3 by A15, Th17;
hence <*2,1,3*> in Permutations 3 by A16, Th18; :: thesis: verum

end;

<*3,1,2*> in Permutations 3

proof

reconsider h = <*1,2*> as FinSequence of NAT ;
<*3*> ^ h = <*3,1,2*> by FINSEQ_1:60;
hence <*3,1,2*> in Permutations 3 by A9, Th18, FINSEQ_2:62; :: thesis: verum

end;

hence x in Permutations 3 by A8, A9, A10, A11, A13, A14, Th15, FINSEQ_2:62, TARSKI:def 2; :: thesis: verum

end;

then {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} c= Permutations 3 by TARSKI:def 3;
hence Permutations 3 = {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} by A7, XBOOLE_0:def 10; :: thesis: verum