now

let p be set ; :: thesis: ( p in Permutations 2 implies p in {(idseq 2),(Rev (idseq 2))} )
assume p in Permutations 2 ; :: thesis: p in {(idseq 2),(Rev (idseq 2))}
then reconsider q = p as Permutation of (Seg 2) by MATRIX_2:def 11;
A1: ( q is Function of (Seg 2),(Seg 2) & rng q = Seg 2 ) by FUNCT_2:def 3;
A2: dom q = Seg 2 by FUNCT_2:67;
then reconsider q = q as FinSequence by FINSEQ_1:def 2;
( q = idseq 2 or q = Rev (idseq 2) ) by A1, A2, Th3;
hence p in {(idseq 2),(Rev (idseq 2))} by TARSKI:def 2; :: thesis: verum

end;

then A3: Permutations 2 c= {(idseq 2),(Rev (idseq 2))} by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in {(idseq 2),(Rev (idseq 2))} implies x in Permutations 2 )
assume x in {(idseq 2),(Rev (idseq 2))} ; :: thesis: x in Permutations 2
then ( x = idseq 2 or x = Rev (idseq 2) ) by TARSKI:def 2;
hence x in Permutations 2 by Th4, MATRIX_2:def 11; :: thesis: verum

end;

then {(idseq 2),(Rev (idseq 2))} c= Permutations 2 by TARSKI:def 3;
hence Permutations 2 = {(idseq 2),(Rev (idseq 2))} by A3, XBOOLE_0:def 10; :: thesis: verum