---

Step * of Lemma geo-sep-between-eq

∀e:BasicGeometry. ∀a,b,c:Point.  (a_b_c ⇒ a ≠ b ⇒ a ≠ c)
BY
{ (InstLemma `geo-between-sep` [] THEN RepeatFor 2 (ParallelLast) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c:Point.    (a\_b\_c  {}\mRightarrow{}  a  \mneq{}  b  {}\mRightarrow{}  a  \mneq{}  c)


By

---

Latex:
(InstLemma  `geo-between-sep`  []  THEN  RepeatFor  2  (ParallelLast)  THEN  Auto)

---

Home Index