:: deftheorem defines inversions EXCHSORT:def 11 :
for O being RelStr
for A being array of O holds inversions A = { [a,b] where a, b is Element of dom A : ( a in b & not A /. a <= A /. b ) } ;