<ℕ,+> ∈ OCMon
{ BLemma `inj_into_ocmon` THEN Auto⋅ }
∃h:OCMon
∃f:|<ℕ,+>| ⟶ |h|
(IsMonHomInj(<ℕ,+>;h;f)
∧ RelsIso(|<ℕ,+>|;|h|;x,y.↑(x =b y);x,y.↑(x =b y);f)
∧ RelsIso(|<ℕ,+>|;|h|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);f))