---

Step * of Lemma triangle-separation-lemma

∀e:HeytingGeometry. ∀A,B,C:Point.  (A # BC ⇒ CA ≅ CB ⇒ (∃P:Point. (C-A-P ∧ P ≠ B)))
BY
{ Auto }

1
1. e : HeytingGeometry
2. A : Point
3. B : Point
4. C : Point
5. A # BC
6. CA ≅ CB
⊢ ∃P:Point. (C-A-P ∧ P ≠ B)

---

Latex:

---

Latex:
\mforall{}e:HeytingGeometry.  \mforall{}A,B,C:Point.    (A  \#  BC  {}\mRightarrow{}  CA  \00D0  CB  {}\mRightarrow{}  (\mexists{}P:Point.  (C-A-P  \mwedge{}  P  \mneq{}  B)))


By

---

Latex:
Auto

---

Home Index