---

Step * 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 ∈ LINE
⊢ Colinear(p;fst(m);fst(snd(m)))
BY
{ (EqTypeHD (-1) THENA Auto)⋅ }

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. [%3] : (m ∈ Line) ∧ (l ∈ Line) ∧ 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
\mvdash{}  Colinear(p;fst(m);fst(snd(m)))


By

---

Latex:
(EqTypeHD  (-1)  THENA  Auto)\mcdot{}

---

Home Index