---

Step * 1 of Lemma geo-zero-lt-iff


1. e : BasicGeometry
2. u : Point
3. v : Point
4. ∀[x:Length]. (x + 0 = x ∈ Length)
5. ∃a,b:Point. (a ≠ b ∧ |ab| ≤ |uv|)
⊢ u ≠ v
BY
{ ExRepD }

1
1. e : BasicGeometry
2. u : Point
3. v : Point
4. ∀[x:Length]. (x + 0 = x ∈ Length)
5. a : Point
6. b : Point
7. a ≠ b
8. |ab| ≤ |uv|
⊢ u ≠ v

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  u  :  Point
3.  v  :  Point
4.  \mforall{}[x:Length].  (x  +  0  =  x)
5.  \mexists{}a,b:Point.  (a  \mneq{}  b  \mwedge{}  |ab|  \mleq{}  |uv|)
\mvdash{}  u  \mneq{}  v


By

---

Latex:
ExRepD

---

Home Index