__The ladder theorem__

Let `p` and `q` be two column vectors of the same (finite) length. Let [`p` ≥ `q`] denote that in each row, the `p`-element is at least the `q`-element , i.e.

[

p≥q] ≡ 〈∀i ::p.i≥q.i〉

Let sort.`w` denote the result of sorting column vector `w` in ascending order. Then the ladder theorem states

(0) [`p` ≥ `q`] ⇒ [sort.`p` ≥ sort.`q`]

__Proof__ We observe for any `x` and positive `n`

the `n`th element of sort.`p` is ≤ `x`

≡` `{ sort.`p` is in ascending order }

sort.`p` contains at least `n` elements ≤ `x`

≡` `{ `p` is a permutation of sort.`p` }

`p` contains at least `n` elements ≤ `x`

⇒` `{ [`p` ≥ `q`], the antecedent of (0) }

`q` contains at least `n` elements ≤ `x`

≡` `{ `q` is a permutation of sort.`q` }

sort.`q` contains at least `n` elements ≤ `x`

≡` `{ sort.`q` is in ascending order }

the `n`th element of sort.`q` is ≤ `x` ,

and since the above calculation derives that, as a consequence of [`p` ≥ `q`], its first line implies its last line for any x , it captures by "indirect order" the elementwise demonstration of [sort.`p` ≥ sort.`q`] .