---

Step * of Lemma geo-le-cases

∀e:BasicGeometry. ∀[p,q:Length].  (¬¬(p ≤ q ∨ q ≤ p))
BY
{ (Auto THEN (D 0 THENA Auto) THEN UseWitness ⌜Ax⌝⋅ THEN (D 3 THEN D 2) THEN Assert ⌜False⌝⋅ THEN Auto) }

1
.....assertion..... 
1. e : BasicGeometry
2. p : Base
3. p1 : Base
4. p = p1 ∈ pertype(λx,y. ((x ∈ {p:Point| O_X_p} ) ∧ (y ∈ {p:Point| O_X_p} ) ∧ x ≡ y))
5. p ∈ {p:Point| O_X_p} 
6. p1 ∈ {p:Point| O_X_p} 
7. p ≡ p1
8. q : Base
9. q1 : Base
10. q = q1 ∈ pertype(λx,y. ((x ∈ {p:Point| O_X_p} ) ∧ (y ∈ {p:Point| O_X_p} ) ∧ x ≡ y))
11. q ∈ {p:Point| O_X_p} 
12. q1 ∈ {p:Point| O_X_p} 
13. q ≡ q1
14. ¬(p ≤ q ∨ q ≤ p)
⊢ False

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}[p,q:Length].    (\mneg{}\mneg{}(p  \mleq{}  q  \mvee{}  q  \mleq{}  p))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
  THEN  (D  3  THEN  D  2)
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index