---

Step * 1 1 1 1 of Lemma geo-line-eq-geoline


1. e : EuclideanPlane
2. l : Line
3. m : Line
⊢ Colinear(fst(l);fst(m);fst(snd(m))) ⇒ Colinear(fst(snd(l));fst(m);fst(snd(m))) ⇒ l ≡ m
BY
{ EAuto 1 }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  l  :  Line
3.  m  :  Line
\mvdash{}  Colinear(fst(l);fst(m);fst(snd(m)))  {}\mRightarrow{}  Colinear(fst(snd(l));fst(m);fst(snd(m)))  {}\mRightarrow{}  l  \mequiv{}  m


By

---

Latex:
EAuto  1

---

Home Index