---

Step * 2 of Lemma geo-incident_functionality


1. e1 : EuclideanPlane
2. m : Line
3. p : Point
4. q : Point
5. p ≡ q
6. ∀l:Line. ((l = m ∈ LINE) ⇒ Colinear(q;fst(l);fst(snd(l))))
7. l : Line
8. l = m ∈ LINE
9. Colinear(q;fst(l);fst(snd(l)))
⊢ Colinear(p;fst(l);fst(snd(l)))
BY
{ (RWO "5" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  e1  :  EuclideanPlane
2.  m  :  Line
3.  p  :  Point
4.  q  :  Point
5.  p  \mequiv{}  q
6.  \mforall{}l:Line.  ((l  =  m)  {}\mRightarrow{}  Colinear(q;fst(l);fst(snd(l))))
7.  l  :  Line
8.  l  =  m
9.  Colinear(q;fst(l);fst(snd(l)))
\mvdash{}  Colinear(p;fst(l);fst(snd(l)))


By

---

Latex:
(RWO  "5"  0  THEN  Auto)

---

Home Index