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 A1: ( [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 A1, Th72;
then ((R,x,y) incl) .: (inversions (Swap (R,x,y))) c= w ;
then reconsider hws = ((R,x,y) incl) .: (inversions (Swap (R,x,y))) as finite set ;
card hws < card w by A1, Th72, TREES_1:6;
then A2: card hws in Segm (card w) by NAT_1:44;
A3: ( x in dom R & y in dom R & x in y ) by A1, Th46;
A4: not R is empty by A1;
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 A3, A4, Th71; :: 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 Th47;
then inversions (Swap (R,x,y)) c= dom ((R,x,y) incl) by A3, A4, Th61;
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 A2, CARD_1:5; :: thesis: verum