---

Step * of Lemma symmetry-preserves-congruence

∀e:BasicGeometry. ∀A,P,Q,p,q:Point.  (p=A=P ⇒ q=A=Q ⇒ PQ ≅ pq)
BY
{ (InstLemma `geo-midpoint-diagonals-congruent` [] THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}A,P,Q,p,q:Point.    (p=A=P  {}\mRightarrow{}  q=A=Q  {}\mRightarrow{}  PQ  \mcong{}  pq)


By

---

Latex:
(InstLemma  `geo-midpoint-diagonals-congruent`  []  THEN  Auto)

---

Home Index