---

Step * of Lemma seg-midpoints-equal-flip

∀e:BasicGeometry. ∀P,Q,A,X:Point.  ((P=A=X ∧ X=A=Q) ⇒ P ≡ Q)
BY
{ Auto }

1
1. e : BasicGeometry
2. P : Point
3. Q : Point
4. A : Point
5. X : Point
6. P=A=X
7. X=A=Q
⊢ P ≡ Q

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}P,Q,A,X:Point.    ((P=A=X  \mwedge{}  X=A=Q)  {}\mRightarrow{}  P  \mequiv{}  Q)


By

---

Latex:
Auto

---

Home Index