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 & inversions R is finite holds
card (inversions (Swap (R,x,y))) in card (inversions R)
let O be non empty connected Poset; :: thesis: for R being array of O st [x,y] in inversions R & inversions R is finite holds
card (inversions (Swap (R,x,y))) in card (inversions R)
let R be array of O; :: thesis: ( [x,y] in inversions R & inversions R is finite implies card (inversions (Swap (R,x,y))) in card (inversions R) )
set s = Swap (R,x,y);
set h = (R,x,y) incl ;
set ws = inversions (Swap (R,x,y));
assume Z0: ( [x,y] in inversions R & inversions R is finite ) ; :: thesis: card (inversions (Swap (R,x,y))) in card (inversions R)
then reconsider w = inversions R as finite set ;
((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R by Z0, MAIN1;
then ((R,x,y) incl) .: (inversions (Swap (R,x,y))) c= w by XBOOLE_0:def 8;
then reconsider hws = ((R,x,y) incl) .: (inversions (Swap (R,x,y))) as finite set ;
card hws < card w by Z0, MAIN1, TREES_1:6;
then A3: card hws in card w by NAT_1:44;
A1: ( x in dom R & y in dom R & x in y ) by Z0, TW0;
A2: not R is empty by Z0;
inversions (Swap (R,x,y)),((R,x,y) incl) .: (inversions (Swap (R,x,y))) are_equipotent

proof

take hw = ((R,x,y) incl) | (inversions (Swap (R,x,y))); :: according to WELLORD2:def 4 :: thesis: ( hw is one-to-one & proj1 hw = inversions (Swap (R,x,y)) & proj2 hw = ((R,x,y) incl) .: (inversions (Swap (R,x,y))) )
thus hw is one-to-one by A1, A2, one2one; :: thesis: ( proj1 hw = inversions (Swap (R,x,y)) & proj2 hw = ((R,x,y) incl) .: (inversions (Swap (R,x,y))) )
dom (Swap (R,x,y)) = dom R by FUNCT_7:99;
then inversions (Swap (R,x,y)) c= [:(dom R),(dom R):] by TW1;
then inversions (Swap (R,x,y)) c= dom ((R,x,y) incl) by A1, A2, FF2;
hence dom hw = inversions (Swap (R,x,y)) by RELAT_1:62; :: thesis: proj2 hw = ((R,x,y) incl) .: (inversions (Swap (R,x,y)))
thus proj2 hw = ((R,x,y) incl) .: (inversions (Swap (R,x,y))) by RELAT_1:115; :: thesis: verum

end;

hence card (inversions (Swap (R,x,y))) in card (inversions R) by A3, CARD_1:5; :: thesis: verum