---

Step * 1 1 1 1 1 1 2 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(Xab)
⊢ a < b ∨ b < a ∨ (a = b ∈ Length)
BY
{ (OrLeft THEN Auto) }

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(Xab)
⊢ a < b

---

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(Xab)
\mvdash{}  a  <  b  \mvee{}  b  <  a  \mvee{}  (a  =  b)


By

---

Latex:
(OrLeft  THEN  Auto)

---

Home Index