let x, y, z be set ; :: thesis: for O being non empty connected Poset
for R being array of O st [x,y] in inversions R holds
( [z,x] in inversions R iff ( z in x & [z,y] in inversions (Swap (R,x,y)) ) )
let O be non empty connected Poset; :: thesis: for R being array of O st [x,y] in inversions R holds
( [z,x] in inversions R iff ( z in x & [z,y] in inversions (Swap (R,x,y)) ) )
let R be array of O; :: thesis: ( [x,y] in inversions R implies ( [z,x] in inversions R iff ( z in x & [z,y] in inversions (Swap (R,x,y)) ) ) )
assume [x,y] in inversions R ; :: thesis: ( [z,x] in inversions R iff ( z in x & [z,y] in inversions (Swap (R,x,y)) ) )
then A1: ( x in dom R & y in dom R & x in y & R /. x > R /. y ) by Th46;
A2: dom (Swap (R,x,y)) = dom R by FUNCT_7:99;

hereby :: thesis: ( z in x & [z,y] in inversions (Swap (R,x,y)) implies [z,x] in inversions R )

assume [z,x] in inversions R ; :: thesis: ( z in x & [z,y] in inversions (Swap (R,x,y)) )
then A3: ( z in dom R & z in x & R /. z > R /. x ) by Th46;
then A4: z in y by A1, ORDINAL1:10;
( (Swap (R,x,y)) /. y = R /. x & (Swap (R,x,y)) /. z = R /. z ) by A1, A3, Th32, Th34;
hence ( z in x & [z,y] in inversions (Swap (R,x,y)) ) by A1, A2, A3, A4; :: thesis: verum

end;

assume A5: ( z in x & [z,y] in inversions (Swap (R,x,y)) ) ; :: thesis: [z,x] in inversions R
then A6: ( z in dom R & z in y & (Swap (R,x,y)) /. z > (Swap (R,x,y)) /. y ) by A2, Th46;
then ( z <> x & z <> y ) by A5;
then ( (Swap (R,x,y)) /. y = R /. x & (Swap (R,x,y)) /. z = R /. z ) by A1, A6, Th32, Th34;
hence [z,x] in inversions R by A1, A6, A5; :: thesis: verum