---

Step * 1 of Lemma not-lt-or


1. g : EuclideanPlane
2. p : Length
3. q : Length
4. ¬(p < q ∨ q < p ∨ (p = q ∈ Length))
⊢ False
BY
{ (UseWitness ⌜Ax⌝⋅ THEN (D 3 THEN D 2) THEN Assert ⌜False⌝⋅ THEN Auto) }

1
.....assertion..... 
1. g : EuclideanPlane
2. p : Base
3. p1 : Base
4. p = p1 ∈ (x,y:{p:Point| B(OXp)} //x ≡ y)
5. p ∈ {p:Point| B(OXp)} 
6. p1 ∈ {p:Point| B(OXp)} 
7. p ≡ p1
8. q : Base
9. q1 : Base
10. q = q1 ∈ (x,y:{p:Point| B(OXp)} //x ≡ y)
11. q ∈ {p:Point| B(OXp)} 
12. q1 ∈ {p:Point| B(OXp)} 
13. q ≡ q1
14. ¬(p < q ∨ q < p ∨ (p = q ∈ Length))
⊢ False

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  p  :  Length
3.  q  :  Length
4.  \mneg{}(p  <  q  \mvee{}  q  <  p  \mvee{}  (p  =  q))
\mvdash{}  False


By

---

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

---

Home Index