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


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

1
1. EuclideanPlane
2. Point
3. B(OXa)
4. Point
5. B(OXb)
6. {p:Point| B(OXp)}  ⊆Length
7. a ∈ Length
8. b ∈ Length
9. b
10. B(Xab)
⊢ ∃a@0,b@0:Point. (a@0 b@0 ∧ |a@0b@0| ≤ 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


By


Latex:
Unfold  `geo-lt`  0




Home Index