now :: thesis: for p being object st p in Permutations 2 holds

p in {(idseq 2),(Rev (idseq 2))}

then A3:
Permutations 2 c= {(idseq 2),(Rev (idseq 2))}
by TARSKI:def 3;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;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

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

x in Permutations 2

then
{(idseq 2),(Rev (idseq 2))} c= Permutations 2
by TARSKI:def 3;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;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

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