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 A1: [x,y] in inversions R ; :: thesis: card (inversions (Swap (R,x,y))) < card (inversions R)
card (inversions (Swap (R,x,y))) in Segm (card (inversions R)) by A1, Th73;
hence card (inversions (Swap (R,x,y))) < card (inversions R) by NAT_1:44; :: thesis: verum