for i, j, n being Nat st i < j & i in Seg n & j in Seg n holds
ex tr being Element of Permutations n st
( tr is being_transposition & tr . i = j )