theorem Th31: :: MATRIX_9:31

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