let x, y be set ; 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; 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; ( [x,y] in inversions R implies card (inversions (Swap (R,x,y))) < card (inversions R) )
assume A1:
[x,y] in inversions R
; 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; verum