---

Step * of Lemma geo-midpoint-symmetry

No Annotations
∀e:BasicGeometry. ∀m,a,b:Point.  (a=m=b ⇒ b=m=a)
BY
{ (Unfold `geo-midpoint` 0 THEN Auto) }

1
1. e : BasicGeometry
2. m : Point
3. a : Point
4. b : Point
5. B(amb)
6. am ≅ mb
7. B(bma)
⊢ bm ≅ ma

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:BasicGeometry.  \mforall{}m,a,b:Point.    (a=m=b  {}\mRightarrow{}  b=m=a)


By

---

Latex:
(Unfold  `geo-midpoint`  0  THEN  Auto)

---

Home Index