theorem :: MATRIX_9:32

for p being Permutation of (Seg 3) st p = <*3,2,1*> holds
p is being_transposition