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*> )
p in Permutations 3 by MATRIX_1:def 12;
then A1: ( 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;
assume p is being_transposition ; :: thesis: ( p = <*2,1,3*> or p = <*1,3,2*> or p = <*3,2,1*> )
hence ( p = <*2,1,3*> or p = <*1,3,2*> or p = <*3,2,1*> ) by A1, Th33, Th34, Th35, FINSEQ_2:53; :: thesis: verum