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

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