---

Step * of Lemma two-mul

∀[x:Top]. (x + x ~ 2 * x)
BY
{ Assert ⌜∀[x:ℤ]. (x + x ~ 2 * x)⌝⋅ }

1
.....assertion..... 
∀[x:ℤ]. (x + x ~ 2 * x)

2
1. ∀[x:ℤ]. (x + x ~ 2 * x)
⊢ ∀[x:Top]. (x + x ~ 2 * x)

---

Latex:

---

Latex:
\mforall{}[x:Top].  (x  +  x  \msim{}  2  *  x)


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}[x:\mBbbZ{}].  (x  +  x  \msim{}  2  *  x)\mkleeneclose{}\mcdot{}

---

Home Index