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

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

assume Z1: ( y in z & [x,z] in inversions R ) ; :: thesis: [y,z] in inversions (Swap (R,x,y))
then A2: ( z in dom R & x in z & R /. z < R /. x ) by TW0;
then ( z <> x & z <> y ) by Z1;
then ( (Swap (R,x,y)) /. y = R /. x & (Swap (R,x,y)) /. z = R /. z ) by A0, A2, TSb2, TSc2;
hence [y,z] in inversions (Swap (R,x,y)) by A0, A1, A2, Z1; :: thesis: verum

end;

assume [y,z] in inversions (Swap (R,x,y)) ; :: thesis: ( y in z & [x,z] in inversions R )
then A2: ( z in dom R & y in z & (Swap (R,x,y)) /. y > (Swap (R,x,y)) /. z ) by A1, TW0;
then A3: x in z by A0, ORDINAL1:10;
( (Swap (R,x,y)) /. y = R /. x & (Swap (R,x,y)) /. z = R /. z ) by A0, TSb2, TSc2, A2;
hence ( y in z & [x,z] in inversions R ) by A0, A2, A3; :: thesis: verum