---

Step * of Lemma midpoint-of-equidistant-points-is-perp

∀e:EuclideanPlane. ∀u:Point. ∀v:{v:Point| u # v} . ∀c:{c:Point| c # uv} .  (cu ≅ cv ⇒ (∀m:Point. (u=m=v ⇒ uv  ⊥m mc)))
BY
{ Auto }

1
1. e : EuclideanPlane
2. u : Point
3. v : {v:Point| u # v} 
4. c : {c:Point| c # uv} 
5. cu ≅ cv
6. m : Point
7. u=m=v
⊢ uv  ⊥m mc

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}u:Point.  \mforall{}v:\{v:Point|  u  \#  v\}  .  \mforall{}c:\{c:Point|  c  \#  uv\}  .
    (cu  \mcong{}  cv  {}\mRightarrow{}  (\mforall{}m:Point.  (u=m=v  {}\mRightarrow{}  uv    \mbot{}m  mc)))


By

---

Latex:
Auto

---

Home Index