---

Step * of Lemma r2-line-eq_weakening

∀l,m:r2-line.  ((l = m ∈ r2-line) ⇒ r2-line-eq(l;m))
BY
{ Auto }

1
1. l : r2-line@i
2. m : r2-line@i
3. l = m ∈ r2-line
⊢ r2-line-eq(l;m)

---

Latex:

---

Latex:
\mforall{}l,m:r2-line.    ((l  =  m)  {}\mRightarrow{}  r2-line-eq(l;m))


By

---

Latex:
Auto

---

Home Index