---

Step * 1 1 1 1 1 1 1 1 of Lemma not-lt-or


1. g : EuclideanPlane
2. a : Point
3. B(OXa)
4. b : Point
5. B(OXb)
6. {p:Point| B(OXp)}  ⊆r Length
7. a ∈ Length
8. b ∈ Length
9. a # b
10. B(Xba)
⊢ b < a
BY
{ Unfold `geo-lt` 0 }

1
1. g : EuclideanPlane
2. a : Point
3. B(OXa)
4. b : Point
5. B(OXb)
6. {p:Point| B(OXp)}  ⊆r Length
7. a ∈ Length
8. b ∈ Length
9. a # b
10. B(Xba)
⊢ ∃a@0,b@0:Point. (a@0 # b@0 ∧ b + |a@0b@0| ≤ a)

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  B(OXa)
4.  b  :  Point
5.  B(OXb)
6.  \{p:Point|  B(OXp)\}    \msubseteq{}r  Length
7.  a  \mmember{}  Length
8.  b  \mmember{}  Length
9.  a  \#  b
10.  B(Xba)
\mvdash{}  b  <  a


By

---

Latex:
Unfold  `geo-lt`  0

---

Home Index