---

Step * 1 1 of Lemma geo-incident-line


1. e : EuclideanPlane
2. Line ⊆r LINE
3. p : Point
4. l : Line
5. Colinear(p;fst(l);fst(snd(l)))
6. m : Line
7. m = l ∈ pertype(λl,m. ((l ∈ Line) ∧ (m ∈ Line) ∧ l ≡ m))
8. [%3] : (m ∈ Line) ∧ (l ∈ Line) ∧ m ≡ l
⊢ Colinear(p;fst(m);fst(snd(m)))
BY
{ (Unhide THEN EAuto 1) }

1
1. e : EuclideanPlane
2. Line ⊆r LINE
3. p : Point
4. l : Line
5. Colinear(p;fst(l);fst(snd(l)))
6. m : Line
7. m = l ∈ pertype(λl,m. ((l ∈ Line) ∧ (m ∈ Line) ∧ l ≡ m))
8. m ∈ Line
9. l ∈ Line
10. m ≡ l
⊢ Colinear(p;fst(m);fst(snd(m)))

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  Line  \msubseteq{}r  LINE
3.  p  :  Point
4.  l  :  Line
5.  Colinear(p;fst(l);fst(snd(l)))
6.  m  :  Line
7.  m  =  l
8.  [\%3]  :  (m  \mmember{}  Line)  \mwedge{}  (l  \mmember{}  Line)  \mwedge{}  m  \mequiv{}  l
\mvdash{}  Colinear(p;fst(m);fst(snd(m)))


By

---

Latex:
(Unhide  THEN  EAuto  1)

---

Home Index