---

Step * of Lemma geo-congruent-mid-exists

∀e:HeytingGeometry. ∀A,B,C:Point.  (A # BC ⇒ CA ≅ CB ⇒ (∃x:Point. A=x=B))
BY
{ ((Auto THEN Using [`b',⌜C⌝] (BLemma  `isosceles-mid-exists`)⋅) THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  Using  [`b',\mkleeneopen{}C\mkleeneclose{}]  (BLemma    `isosceles-mid-exists`)\mcdot{})  THEN  Auto)

---

Home Index