theorem Th46: :: EXCHSORT:46

for O being non empty connected Poset
for R being array of O
for x being object
for y being set holds
( [x,y] in inversions R iff ( x in dom R & y in dom R & x in y & R /. x > R /. y ) )