---

Step * of Lemma geo-between-implies-sep

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

1
1. e : BasicGeometry
2. a : Point
3. ∀b,x:Point.  (a_x_b ⇒ a ≠ x ⇒ a ≠ b)
⊢ ∀b,c:Point.  (a ≠ b ⇒ a_b_c ⇒ a ≠ c)

---

Latex:

---

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


By

---

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

---

Home Index