---

Step * of Lemma geo-colinear-incident

∀[e:EuclideanPlane]. ∀[l:LINE]. ∀[a,b,v:Point].  (a ≠ b ⇒ Colinear(a;b;v) ⇒ a I l ⇒ b I l ⇒ v I l)
BY
{ Auto }

1
1. e : EuclideanPlane
2. l : LINE
3. a : Point
4. b : Point
5. v : Point
6. a ≠ b
7. Colinear(a;b;v)
8. a I l
9. b I l
⊢ v I l

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index