---

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


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)))}
BY
{ (((D 2 THEN D 3) THEN D 5 THEN D 6) THEN All Reduce⋅) }

1
1. g : EuclideanPlane
2. x : Point
3. y : Point
4. l2 : x ≠ y
5. x1 : Point
6. y1 : Point
7. m2 : x1 ≠ y1
8. <x, y, l2> ≡ <x1, y1, m2>
⊢ {Colinear(x;y;x1) ∧ Colinear(x;y;y1)}

---

Latex:

---

Latex:

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


By

---

Latex:
(((D  2  THEN  D  3)  THEN  D  5  THEN  D  6)  THEN  All  Reduce\mcdot{})

---

Home Index