---

Step * 1 1 1 of Lemma geo-le-cases


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
BY
{ ((Assert (a ∈ Length) ∧ (b ∈ Length) BY Auto) THEN DSetVars) }

1
1. e : BasicGeometry
2. a : Point
3. O_X_a
4. b : Point
5. O_X_b
6. {p:Point| O_X_p}  ⊆r Length
7. ¬(a ≤ b ∨ b ≤ a)
8. (a ∈ Length) ∧ (b ∈ Length)
⊢ False

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  (a  \mmember{}  Length)  \mwedge{}  (b  \mmember{}  Length)  BY  Auto)  THEN  DSetVars)

---

Home Index