let p be Permutation of (Seg 3); :: thesis: ( not p is being_transposition or p = <*2,1,3*> or p = <*1,3,2*> or p = <*3,2,1*> )
assume A1: p is being_transposition ; :: thesis: ( p = <*2,1,3*> or p = <*1,3,2*> or p = <*3,2,1*> )
p in Permutations 3 by MATRIX_2:def 11;
then ( p = <*1,2,3*> or p = <*2,1,3*> or p = <*2,3,1*> or p = <*3,1,2*> or p = <*3,2,1*> or p = <*1,3,2*> ) by Th19, ENUMSET1:def 4;
hence ( p = <*2,1,3*> or p = <*1,3,2*> or p = <*3,2,1*> ) by A1, Th33, Th34, Th35, FINSEQ_2:62; :: thesis: verum