---

Step * of Lemma tarski-erect-perp-or

∀e:HeytingGeometry. ∀a,b,c:Point.  (c # ba ⇒ (∃p,t:Point. (((ab ⊥ pa ∨ ab ⊥ pb) ∧ Colinear(a;b;t)) ∧ p-t-c)))
BY
{ Auto }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. c # ba
⊢ ∃p,t:Point. (((ab ⊥ pa ∨ ab ⊥ pb) ∧ Colinear(a;b;t)) ∧ p-t-c)

---

Latex:

---

Latex:
\mforall{}e:HeytingGeometry.  \mforall{}a,b,c:Point.
    (c  \#  ba  {}\mRightarrow{}  (\mexists{}p,t:Point.  (((ab  \mbot{}  pa  \mvee{}  ab  \mbot{}  pb)  \mwedge{}  Colinear(a;b;t))  \mwedge{}  p-t-c)))


By

---

Latex:
Auto

---

Home Index