now :: thesis: for p being object st p in Permutations 2 holds
p in {(idseq 2),(Rev (idseq 2))}

let p be object ; :: 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_1:def 12;
A1: rng q = Seg 2 by FUNCT_2:def 3;
A2: dom q = Seg 2 by FUNCT_2:52;
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 :: thesis: for x being object st x in {(idseq 2),(Rev (idseq 2))} holds
x in Permutations 2

let x be object ; :: 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_1:def 12; :: 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