---

Step * of Lemma eq_int-wf-partial2

∀[x,y:partial(ℤ)].  ((x =z y) ∈ partial(𝔹))
BY
{ ((UnivCD THENA Auto) THEN BLemma `eq_int-wf-partial` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x,y:partial(\mBbbZ{})].    ((x  =\msubz{}  y)  \mmember{}  partial(\mBbbB{}))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  BLemma  `eq\_int-wf-partial`  THEN  Auto)

---

Home Index