let x, y, z, t be set ; :: thesis: 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)) )
let O be non empty connected Poset; :: thesis: 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)) )
let R be array of O; :: thesis: ( x in dom R & y in dom R & z <> x & z <> y & t <> x & t <> y implies ( [z,t] in inversions R iff [z,t] in inversions (Swap (R,x,y)) ) )
set s = Swap (R,x,y);
assume ( x in dom R & y in dom R & z <> x & z <> y & t <> x & t <> y ) ; :: thesis: ( [z,t] in inversions R iff [z,t] in inversions (Swap (R,x,y)) )
then A1: ( ( z in dom R implies (Swap (R,x,y)) /. z = R /. z ) & ( t in dom R implies (Swap (R,x,y)) /. t = R /. t ) & dom (Swap (R,x,y)) = dom R ) by Th34, FUNCT_7:99;
hereby :: thesis: ( [z,t] in inversions (Swap (R,x,y)) implies [z,t] in inversions R )
assume [z,t] in inversions R ; :: thesis: [z,t] in inversions (Swap (R,x,y))
then ( z in dom R & t in dom R & z in t & R /. z > R /. t ) by Th46;
hence [z,t] in inversions (Swap (R,x,y)) by A1; :: thesis: verum
end;
assume [z,t] in inversions (Swap (R,x,y)) ; :: thesis: [z,t] in inversions R
then ( z in dom R & t in dom R & z in t & (Swap (R,x,y)) /. z > (Swap (R,x,y)) /. t ) by A1, Th46;
hence [z,t] in inversions R by A1; :: thesis: verum