preordToCat.proof_1

theorem preordToCat.proof_1 : ∀ {X Y : Preord} (f : X ⟶ Y), Monotone ⇑f

This theorem states that for every pair of objects `X` and `Y` in the category of preorders (`Preord`), any morphism `f` from `X` to `Y` is monotone. In other words, if `a` and `b` are elements of `X` such that `a` is less than or equal to `b`, then the image of `a` under `f` is less than or equal to the image of `b` under `f`.

More concisely: For every morphism `f` in the category of preorders `Preord`, if `a ≤ b` in domain `X` of `f`, then `f(a) ≤ f(b)` in the codomain `Y` of `f`.