---

Step * of Lemma geo-strict-between-sep1

∀e:BasicGeometry-. ∀a,b,c:Point.  (a-b-c ⇒ a ≠ c)
BY
{ (Auto THEN D -1 THEN EAuto 1) }

1
1. e : BasicGeometry-
2. a : Point
3. b : Point
4. c : Point
5. a_b_c
6. a ≠ b
7. b ≠ c
⊢ a ≠ c

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  D  -1  THEN  EAuto  1)

---

Home Index