---

Step * of Lemma geo-between-sep

∀g:EuclideanPlane. ∀a,b,x:Point.  (a_x_b ⇒ a ≠ x ⇒ a ≠ b)
BY
{ (Auto THEN InstLemma `geo-ge-sep` [⌜g⌝;⌜a⌝;⌜x⌝;⌜a⌝;⌜b⌝]⋅ THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,x:Point.    (a\_x\_b  {}\mRightarrow{}  a  \mneq{}  x  {}\mRightarrow{}  a  \mneq{}  b)


By

---

Latex:
(Auto  THEN  InstLemma  `geo-ge-sep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)

---

Home Index