---

Step * of Lemma segment-intersection

∀e:HeytingGeometry. ∀a,b,c:Point.  (c # ab ⇒ (∃p,q:Point. (Colinear(a;b;p) ∧ c-p-q)))
BY
{ Auto }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. c # ab
⊢ ∃p,q:Point. (Colinear(a;b;p) ∧ c-p-q)

---

Latex:

---

Latex:
\mforall{}e:HeytingGeometry.  \mforall{}a,b,c:Point.    (c  \#  ab  {}\mRightarrow{}  (\mexists{}p,q:Point.  (Colinear(a;b;p)  \mwedge{}  c-p-q)))


By

---

Latex:
Auto

---

Home Index