---

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


1. g : EuclideanPlane
2. a : {p:Point| B(OXp)} 
3. b : {p:Point| B(OXp)} 
⊢ (¬(a < b ∨ b < a ∨ (a = b ∈ Length))) ⇒ False
BY
{ ((Assert {p:Point| B(OXp)}  ⊆r Length BY (Unfold `geo-length-type` 0 THEN Auto)) THEN (D 0 THENA Auto)) }

1
1. g : EuclideanPlane
2. a : {p:Point| B(OXp)} 
3. b : {p:Point| B(OXp)} 
4. {p:Point| B(OXp)}  ⊆r Length
5. ¬(a < b ∨ b < a ∨ (a = b ∈ Length))
⊢ False

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  \{p:Point|  B(OXp)\} 
3.  b  :  \{p:Point|  B(OXp)\} 
\mvdash{}  (\mneg{}(a  <  b  \mvee{}  b  <  a  \mvee{}  (a  =  b)))  {}\mRightarrow{}  False


By

---

Latex:
((Assert  \{p:Point|  B(OXp)\}    \msubseteq{}r  Length  BY
                (Unfold  `geo-length-type`  0  THEN  Auto))
  THEN  (D  0  THENA  Auto)
  )

---

Home Index