theorem Th52: :: EXCHSORT:52

for x, y, z, t being set
for O being non empty connected Poset
for R being array of O st x in dom R & y in dom R & z <> x & z <> y & t <> x & t <> y holds
( [z,t] in inversions R iff [z,t] in inversions (Swap (R,x,y)) )