now

let x be set ; :: thesis: ( x in {(idseq 2),<*2,1*>} implies x in Permutations 2 )
assume A1: x in {(idseq 2),<*2,1*>} ; :: thesis: x in Permutations 2

now

per cases ( x = idseq 2 or x = <*2,1*> ) by A1, TARSKI:def 2;

case x = idseq 2 ; :: thesis: x in Permutations 2

hence x in Permutations 2 by MATRIX_2:def 11; :: thesis: verum

end;

case A2: x = <*2,1*> ; :: thesis: x in Permutations 2

<*2,1*> is Permutation of (Seg 2) by Th2;
hence x in Permutations 2 by A2, MATRIX_2:def 11; :: thesis: verum

end;

end;

end;

hence x in Permutations 2 ; :: thesis: verum

end;

then A3: {(idseq 2),<*2,1*>} c= Permutations 2 by TARSKI:def 3;

now

let p be set ; :: thesis: ( p in Permutations 2 implies p in {(idseq 2),<*2,1*>} )
assume p in Permutations 2 ; :: thesis: p in {(idseq 2),<*2,1*>}
then reconsider q = p as Permutation of (Seg 2) by MATRIX_2:def 11;
( q = <*1,2*> or q = <*2,1*> ) by Th1;
hence p in {(idseq 2),<*2,1*>} by FINSEQ_2:61, TARSKI:def 2; :: thesis: verum

end;

then Permutations 2 c= {(idseq 2),<*2,1*>} by TARSKI:def 3;
hence Permutations 2 = {<*1,2*>,<*2,1*>} by A3, FINSEQ_2:61, XBOOLE_0:def 10; :: thesis: verum