---

Step * 1 of Lemma triangle-separation-lemma


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)
BY
{ ((PropergProlong ⌜C⌝ ⌜A⌝ `X' ⌜A⌝ ⌜B⌝⋅ THEN Auto) THEN (Assert X # BC BY Auto)) }

1
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)

---

Latex:

---

Latex:

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


By

---

Latex:
((PropergProlong  \mkleeneopen{}C\mkleeneclose{}  \mkleeneopen{}A\mkleeneclose{}  `X'  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}B\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  (Assert  X  \#  BC  BY  Auto))

---

Home Index