---

Step * of Lemma geo-line-eq-to-col

∀g:EuclideanPlane. ∀l,m:Line.
  (l ≡ m ⇒ {Colinear(fst(l);fst(snd(l));fst(m)) ∧ Colinear(fst(l);fst(snd(l));fst(snd(m)))})
BY
{ Auto }

1
1. g : EuclideanPlane
2. l : Line
3. m : Line
4. l ≡ m
⊢ {Colinear(fst(l);fst(snd(l));fst(m)) ∧ Colinear(fst(l);fst(snd(l));fst(snd(m)))}

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}l,m:Line.
    (l  \mequiv{}  m  {}\mRightarrow{}  \{Colinear(fst(l);fst(snd(l));fst(m))  \mwedge{}  Colinear(fst(l);fst(snd(l));fst(snd(m)))\})


By

---

Latex:
Auto

---

Home Index