---

Step * of Lemma geo-strict-between-same

∀[e:BasicGeometry-]. ∀[a,b:Point].  (¬a-b-a)
BY
{ ((Auto THEN (D 0 THENA Auto)) THEN FLemma `geo-strict-between-sep1` [-1] THEN Auto) }

1
1. e : BasicGeometry-
2. a : Point
3. b : Point
4. a-b-a
5. a ≠ a
⊢ False

---

Latex:

---

Latex:
\mforall{}[e:BasicGeometry-].  \mforall{}[a,b:Point].    (\mneg{}a-b-a)


By

---

Latex:
((Auto  THEN  (D  0  THENA  Auto))  THEN  FLemma  `geo-strict-between-sep1`  [-1]  THEN  Auto)

---

Home Index