---

Step * 1 1 of Lemma triangle-separation-lemma


1. e : HeytingGeometry
2. A : Point
3. B : Point
4. C : Point
5. A # BC
6. CA ≅ CB
7. X : Point
8. C-A-X
9. AX ≅ AB
10. X # BC
⊢ ∃P:Point. (C-A-P ∧ P ≠ B)
BY
{ (D 0 With ⌜X⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  HeytingGeometry
2.  A  :  Point
3.  B  :  Point
4.  C  :  Point
5.  A  \#  BC
6.  CA  \00D0  CB
7.  X  :  Point
8.  C-A-X
9.  AX  \00D0  AB
10.  X  \#  BC
\mvdash{}  \mexists{}P:Point.  (C-A-P  \mwedge{}  P  \mneq{}  B)


By

---

Latex:
(D  0  With  \mkleeneopen{}X\mkleeneclose{}    THEN  Auto)

---

Home Index