let p be Permutation of (Seg 3); ( 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
; ( 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; verum