now :: thesis: for p being object st p in Permutations 2 holds
p in {(),(Rev ())}
let p be object ; :: thesis: ( p in Permutations 2 implies p in {(),(Rev ())} )
assume p in Permutations 2 ; :: thesis: p in {(),(Rev ())}
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 () ) by A1, A2, Th3;
hence p in {(),(Rev ())} by TARSKI:def 2; :: thesis: verum
end;
then A3: Permutations 2 c= {(),(Rev ())} by TARSKI:def 3;
now :: thesis: for x being object st x in {(),(Rev ())} holds
x in Permutations 2
let x be object ; :: thesis: ( x in {(),(Rev ())} implies x in Permutations 2 )
assume x in {(),(Rev ())} ; :: thesis:
then ( x = idseq 2 or x = Rev () ) by TARSKI:def 2;
hence x in Permutations 2 by ; :: thesis: verum
end;
then {(),(Rev ())} c= Permutations 2 by TARSKI:def 3;
hence Permutations 2 = {(),(Rev ())} by ; :: thesis: verum