---

Step * of Lemma midpoint-sep

∀e:BasicGeometry. ∀A,B,M:Point.  (A ≠ B ⇒ A=M=B ⇒ {A ≠ M ∧ B ≠ M})
BY
{ (((Unfold `geo-midpoint` 0 THEN Unfold `guard` 0) THEN Auto)
   THEN (InstLemma `geo-sep-or` [⌜e⌝;⌜A⌝;⌜B⌝;⌜M⌝]⋅ THENA Auto)
   THEN D -1
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}A,B,M:Point.    (A  \mneq{}  B  {}\mRightarrow{}  A=M=B  {}\mRightarrow{}  \{A  \mneq{}  M  \mwedge{}  B  \mneq{}  M\})


By

---

Latex:
(((Unfold  `geo-midpoint`  0  THEN  Unfold  `guard`  0)  THEN  Auto)
  THEN  (InstLemma  `geo-sep-or`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}M\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  Auto)

---

Home Index