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,y] in inversions R & z in x ) iff [z,x] 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,y] in inversions R & z in x ) iff [z,x] in inversions (Swap (R,x,y)) )
let R be array of O; :: thesis: ( [x,y] in inversions R implies ( ( [z,y] in inversions R & z in x ) iff [z,x] in inversions (Swap (R,x,y)) ) )
set s = Swap (R,x,y);
assume [x,y] in inversions R ; :: thesis: ( ( [z,y] in inversions R & z in x ) iff [z,x] 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;
then A2: ( (Swap (R,x,y)) /. x = R /. y & (Swap (R,x,y)) /. y = R /. x & dom (Swap (R,x,y)) = dom R ) by Th30, Th32, FUNCT_7:99;

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

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

end;

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