---

Step * of Lemma geo-le-zero

∀e:BasicGeometry. ∀[p:Length]. uiff(p ≤ 0;p = 0 ∈ Length)
BY
{ ((UnivCD THENA Auto) THEN Assert ⌜0 = |XX| ∈ Length⌝⋅) }

1
.....assertion..... 
1. e : BasicGeometry
2. p : Length
⊢ 0 = |XX| ∈ Length

2
1. e : BasicGeometry
2. p : Length
3. 0 = |XX| ∈ Length
⊢ uiff(p ≤ 0;p = 0 ∈ Length)

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}[p:Length].  uiff(p  \mleq{}  0;p  =  0)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Assert  \mkleeneopen{}0  =  |XX|\mkleeneclose{}\mcdot{})

---

Home Index