theorem Th30: :: MATRIX_9:30

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