let x, y be set ; :: thesis: for O being non empty connected Poset
for R being array of O st [x,y] in inversions R holds
((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R
let O be non empty connected Poset; :: thesis: for R being array of O st [x,y] in inversions R holds
((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R
let R be array of O; :: thesis: ( [x,y] in inversions R implies ((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R )
assume Z0: [x,y] in inversions R ; :: thesis: ((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R
then A1: ( x in dom R & y in dom R & x in y & R /. x > R /. y ) by TW0;
reconsider T = R as non empty array of O by Z0;
reconsider p = x, q = y as Element of dom T by Z0, TW0;
set j = (R,x,y) incl ;
set k = (T,p,q) incl ;
set s = Swap (R,x,y);
set t = Swap (T,p,q);
set ws = inversions (Swap (R,x,y));
set w = inversions R;
A2: dom (Swap (T,p,q)) = dom T by FUNCT_7:99;
thus ((R,x,y) incl) .: (inversions (Swap (R,x,y))) c= inversions R :: according to XBOOLE_0:def 8 :: thesis: not ((R,x,y) incl) .: (inversions (Swap (R,x,y))) = inversions R

proof

let z be set ; :: according to RELAT_1:def 3 :: thesis: for b₁ being set holds
( not [z,b₁] in ((R,x,y) incl) .: (inversions (Swap (R,x,y))) or [z,b₁] in inversions R )
let t be set ; :: thesis: ( not [z,t] in ((R,x,y) incl) .: (inversions (Swap (R,x,y))) or [z,t] in inversions R )
assume [z,t] in ((R,x,y) incl) .: (inversions (Swap (R,x,y))) ; :: thesis: [z,t] in inversions R
then consider a, b being set such that
A0: ( [a,b] in inversions (Swap (R,x,y)) & [a,b] in dom ((R,x,y) incl) & [z,t] = ((R,x,y) incl) . (a,b) ) by Lem3;
A3: ( a in b & a in dom T & b in dom T ) by A0, A2, TW0;
reconsider a = a, b = b as Element of dom T by A0, A2, TW0;

per cases ( ( a <> p & a <> q & b <> p & b <> q ) or ( a in p & b = p ) or ( a in p & b = q ) or ( a = p & b in q ) or ( a = p & b = q ) or ( a = p & q in b ) or ( a = q & q in b ) or ( p in a & q = b ) ) by A1, A3, Eight;

suppose C1: ( a <> p & a <> q & b <> p & b <> q ) ; :: thesis: [z,t] in inversions R

then [z,t] = [a,b] by A0, A1, Case1;
hence [z,t] in inversions R by A0, C1, TC1; :: thesis: verum

end;

suppose C2: ( a in p & b = p ) ; :: thesis: [z,t] in inversions R

then [z,t] = [a,q] by A0, A1, Case23;
hence [z,t] in inversions R by Z0, A0, C2, TC2; :: thesis: verum

end;

suppose C3: ( a in p & b = q ) ; :: thesis: [z,t] in inversions R

then [z,t] = [a,p] by A0, A1, Case23;
hence [z,t] in inversions R by Z0, A0, C3, TC3; :: thesis: verum

end;

suppose C4: ( a = p & b in q ) ; :: thesis: [z,t] in inversions R

then [z,t] = [a,b] by A3, A0, Case47;
hence [z,t] in inversions R by Z0, A0, C4, TC4; :: thesis: verum

end;

suppose ( a = p & b = q ) ; :: thesis: [z,t] in inversions R

hence [z,t] in inversions R by Z0, A0, A1, Case5; :: thesis: verum

end;

suppose C6: ( a = p & q in b ) ; :: thesis: [z,t] in inversions R

then [z,t] = [q,b] by A0, A1, Case68;
hence [z,t] in inversions R by Z0, A0, C6, TC6; :: thesis: verum

end;

suppose C7: ( a = q & q in b ) ; :: thesis: [z,t] in inversions R

then [z,t] = [p,b] by A0, A1, Case68;
hence [z,t] in inversions R by Z0, A0, C7, TC7; :: thesis: verum

end;

suppose C8: ( p in a & q = b ) ; :: thesis: [z,t] in inversions R

then [z,t] = [a,b] by A0, A3, Case47;
hence [z,t] in inversions R by Z0, A0, C8, TC8; :: thesis: verum

end;

end;

end;

now

assume [x,y] in ((R,x,y) incl) .: (inversions (Swap (R,x,y))) ; :: thesis: [x,y] in inversions (Swap (R,x,y))
then consider a, b being set such that
A0: ( [a,b] in inversions (Swap (R,x,y)) & [a,b] in dom ((R,x,y) incl) & [x,y] = ((R,x,y) incl) . (a,b) ) by Lem3;
A5: ((R,x,y) incl) . (p,q) = [p,q] by A1, Case5;
A6: ( a in b & a in dom T & b in dom T ) by A0, A2, TW0;
reconsider a = a, b = b as Element of dom T by A0, A2, TW0;
( a = p & b = q ) by A1, A0, A5, A6, O2O;
hence [x,y] in inversions (Swap (R,x,y)) by A0; :: thesis: verum

end;

hence not ((R,x,y) incl) .: (inversions (Swap (R,x,y))) = inversions R by Z0, TC5; :: thesis: verum