---

Step * of Lemma isosceles-mid-exists

No Annotations
∀e:HeytingGeometry. ∀a,b,c:Point.  (a # bc ⇒ ab ≅ cb ⇒ (∃x:Point. a=x=c))
BY
{ Auto }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. ab ≅ cb
⊢ ∃x:Point. a=x=c

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:HeytingGeometry.  \mforall{}a,b,c:Point.    (a  \#  bc  {}\mRightarrow{}  ab  \mcong{}  cb  {}\mRightarrow{}  (\mexists{}x:Point.  a=x=c))


By

---

Latex:
Auto

---

Home Index