---

Step * of Lemma geo-incident-line

∀[e:EuclideanPlane]. ∀[p:Point]. ∀[l:Line].  uiff(p I l;Colinear(p;fst(l);fst(snd(l))))
BY
{ (Intro THEN (Assert Line ⊆r LINE BY Auto) THEN Auto THEN (D 0 THEN Auto) THEN RenameVar `m' (-2)) }

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 ∈ LINE
⊢ Colinear(p;fst(m);fst(snd(m)))

---

Latex:

---

Latex:
\mforall{}[e:EuclideanPlane].  \mforall{}[p:Point].  \mforall{}[l:Line].    uiff(p  I  l;Colinear(p;fst(l);fst(snd(l))))


By

---

Latex:
(Intro  THEN  (Assert  Line  \msubseteq{}r  LINE  BY  Auto)  THEN  Auto  THEN  (D  0  THEN  Auto)  THEN  RenameVar  `m'  (-2))

---

Home Index