---

Step * 1 1 of Lemma geo-le-cases


1. e : BasicGeometry
2. a : {p:Point| O_X_p} 
3. b : {p:Point| O_X_p} 
⊢ (¬(a ≤ b ∨ b ≤ a)) ⇒ False
BY
{ ((Assert {p:Point| O_X_p}  ⊆r Length BY (Unfold `geo-length-type` 0 THEN Auto)) THEN (D 0 THENA Auto)) }

1
1. e : BasicGeometry
2. a : {p:Point| O_X_p} 
3. b : {p:Point| O_X_p} 
4. {p:Point| O_X_p}  ⊆r Length
5. ¬(a ≤ b ∨ b ≤ a)
⊢ False

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  \{p:Point|  O\_X\_p\} 
3.  b  :  \{p:Point|  O\_X\_p\} 
\mvdash{}  (\mneg{}(a  \mleq{}  b  \mvee{}  b  \mleq{}  a))  {}\mRightarrow{}  False


By

---

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

---

Home Index