---

Step * of Lemma geo-inner-pasch-ex

∀e:HeytingGeometry. ∀a,b:Point. ∀c:{c:Point| c # ab} . ∀p,q:Point.  (a-p-c ⇒ b-q-c ⇒ (∃x:Point. (b-x-p ∧ a-x-q)))
BY
{ (Unfold `geo-triangle` 0 THEN Auto) }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : {c:Point| c # ab} 
5. p : Point
6. q : Point
7. a-p-c
8. b-q-c
⊢ ∃x:Point. (b-x-p ∧ a-x-q)

---

Latex:

---

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


By

---

Latex:
(Unfold  `geo-triangle`  0  THEN  Auto)

---

Home Index