---

Step * 1 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. m ∈ Line
9. l ∈ Line
10. m ≡ l
⊢ Colinear(p;fst(m);fst(snd(m)))
BY
{ (FLemma `geo-line-eq-to-col` [-1] THEN 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. m ∈ Line
9. l ∈ Line
10. m ≡ l
11. Colinear(fst(m);fst(snd(m));fst(l))
12. Colinear(fst(m);fst(snd(m));fst(snd(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.  m  \mmember{}  Line
9.  l  \mmember{}  Line
10.  m  \mequiv{}  l
\mvdash{}  Colinear(p;fst(m);fst(snd(m)))


By

---

Latex:
(FLemma  `geo-line-eq-to-col`  [-1]  THEN  Auto)

---

Home Index