:: deftheorem defines inversions EXCHSORT:def 12 :
for O being non empty connected Poset
for R being array of O holds inversions R = { [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b ) } ;