---

Step * 1 of Lemma geo-strict-between-same


1. e : BasicGeometry-
2. a : Point
3. b : Point
4. a-b-a
5. a ≠ a
⊢ False
BY
{ (MoveToConcl (-1) THEN Fold `not` 0 THEN Fold `geo-eq` 0) }

1
1. e : BasicGeometry-
2. a : Point
3. b : Point
4. a-b-a
⊢ a ≡ a

---

Latex:

---

Latex:

1.  e  :  BasicGeometry-
2.  a  :  Point
3.  b  :  Point
4.  a-b-a
5.  a  \mneq{}  a
\mvdash{}  False


By

---

Latex:
(MoveToConcl  (-1)  THEN  Fold  `not`  0  THEN  Fold  `geo-eq`  0)

---

Home Index