---

Step * of Lemma at-most-one-midpoint

∀e:BasicGeometry. ∀P,P',A,B:Point.  ((P=A=P' ∧ P=B=P') ⇒ A ≡ B)
BY
{ ((Auto THEN gSeparatedCases ⌜A⌝⌜B⌝⋅) THENA Auto) }

1
1. e : BasicGeometry
2. P : Point
3. P' : Point
4. A : Point
5. B : Point
6. P=A=P'
7. P=B=P'
8. A ≠ B
⊢ A ≡ B

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  gSeparatedCases  \mkleeneopen{}A\mkleeneclose{}\mkleeneopen{}B\mkleeneclose{}\mcdot{})  THENA  Auto)

---

Home Index