---

Step * of Lemma tarski-perp-exists

∀e:HeytingGeometry. ∀a,b,c:Point.  (a # bc ⇒ (∃x:Point. (Colinear(a;b;x) ∧ ab ⊥ cx)))
BY
{ Auto }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. a # bc
⊢ ∃x:Point. (Colinear(a;b;x) ∧ ab ⊥ cx)

---

Latex:

---

Latex:
\mforall{}e:HeytingGeometry.  \mforall{}a,b,c:Point.    (a  \#  bc  {}\mRightarrow{}  (\mexists{}x:Point.  (Colinear(a;b;x)  \mwedge{}  ab  \mbot{}  cx)))


By

---

Latex:
Auto

---

Home Index