---

Step * 1 of Lemma geo-zero-length_wf


1. e : BasicGeometry
⊢ 0 ∈ Length
BY
{ (Unfold `geo-zero-length` 0 THEN MemTypeCD THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
\mvdash{}  0  \mmember{}  Length


By

---

Latex:
(Unfold  `geo-zero-length`  0  THEN  MemTypeCD  THEN  Auto)

---

Home Index