---

Step * 2 1 of Lemma geo-le-zero


1. e : BasicGeometry
2. p : Length
3. 0 = |XX| ∈ Length
⊢ uiff(p ≤ |XX|;p = |XX| ∈ Length)
BY
{ (InstLemma `geo-le-null-segment` [⌜e⌝;⌜p⌝;⌜X⌝] ⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  p  :  Length
3.  0  =  |XX|
\mvdash{}  uiff(p  \mleq{}  |XX|;p  =  |XX|)


By

---

Latex:
(InstLemma  `geo-le-null-segment`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{}]  \mcdot{}  THEN  Auto)

---

Home Index