let x, y be set ; :: thesis: for O being non empty connected Poset
for R being finite array of O st [x,y] in inversions R holds
card (inversions (Swap (R,x,y))) < card (inversions R)
let O be non empty connected Poset; :: thesis: for R being finite array of O st [x,y] in inversions R holds
card (inversions (Swap (R,x,y))) < card (inversions R)
let R be finite array of O; :: thesis: ( [x,y] in inversions R implies card (inversions (Swap (R,x,y))) < card (inversions R) )
assume [x,y] in inversions R ; :: thesis: card (inversions (Swap (R,x,y))) < card (inversions R)
then card (inversions (Swap (R,x,y))) in card (inversions R) by MAIN3;
hence card (inversions (Swap (R,x,y))) < card (inversions R) by NAT_1:44; :: thesis: verum