---

Step * of Lemma geo-strict-between-incident

∀[e:EuclideanPlane]. ∀[l:LINE]. ∀[a,b,v:Point].  (a-v-b ⇒ a I l ⇒ b I l ⇒ v I l)
BY
{ (InstLemma `geo-colinear-incident` [] THEN RepeatFor 5 (ParallelLast') THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[e:EuclideanPlane].  \mforall{}[l:LINE].  \mforall{}[a,b,v:Point].    (a-v-b  {}\mRightarrow{}  a  I  l  {}\mRightarrow{}  b  I  l  {}\mRightarrow{}  v  I  l)


By

---

Latex:
(InstLemma  `geo-colinear-incident`  []  THEN  RepeatFor  5  (ParallelLast')  THEN  Auto)

---

Home Index