---

Step * 1 of Lemma segment-intersection


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)
BY
{ (((gProperProlong ⌜c⌝⌜a⌝`A'⌜c⌝⌜b⌝ ⋅ THENA Auto) THEN (gProperProlong ⌜c⌝⌜b⌝`B'⌜c⌝⌜a⌝ ⋅ THENA Auto)) THEN ExRepD) }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. c # ab
6. A : Point
7. c-a-A
8. aA ≅ cb
9. B : Point
10. c-b-B
11. bB ≅ ca
⊢ ∃p,q:Point. (Colinear(a;b;p) ∧ c-p-q)

---

Latex:

---

Latex:

1.  e  :  HeytingGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  c  \#  ab
\mvdash{}  \mexists{}p,q:Point.  (Colinear(a;b;p)  \mwedge{}  c-p-q)


By

---

Latex:
(((gProperProlong  \mkleeneopen{}c\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}`A'\mkleeneopen{}c\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}  \mcdot{}  THENA  Auto)  THEN  (gProperProlong  \mkleeneopen{}c\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}`B'\mkleeneopen{}c\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}  \mcdot{}  THENA  Auto))
  THEN  ExRepD
  )

---

Home Index