---

Step * of Lemma nat_add_mon_wf2

<ℕ,+> ∈ OCMon
BY
{ BLemma `inj_into_ocmon` THEN Auto⋅ }

1
∃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))

---

Latex:

---

Latex:
<\mBbbN{},+>  \mmember{}  OCMon


By

---

Latex:
BLemma  `inj\_into\_ocmon`  THEN  Auto\mcdot{}

---

Home Index