let p be odd Permutation of (Seg 3); :: thesis: ( p = <*3,2,1*> or p = <*1,3,2*> or p = <*2,1,3*> )
p in Permutations 3 by MATRIX_2:def 11;
hence ( p = <*3,2,1*> or p = <*1,3,2*> or p = <*2,1,3*> ) by Lm5, Lm6, Lm7, Th19, ENUMSET1:def 4; :: thesis: verum