---

Step * of Lemma add-wf-partial

∀[x,y:partial(Base)].  (x + y ∈ partial(ℤ))
BY
{ ((UnivCD THENA Auto) THEN (Assert partial(Base) ⊆r Base BY Auto)) }

1
1. x : partial(Base)
2. y : partial(Base)
3. partial(Base) ⊆r Base
⊢ x + y ∈ partial(ℤ)

---

Latex:

---

Latex:
\mforall{}[x,y:partial(Base)].    (x  +  y  \mmember{}  partial(\mBbbZ{}))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (Assert  partial(Base)  \msubseteq{}r  Base  BY  Auto))

---

Home Index