---

Step * 1 1 of Lemma not-geo-lt

.....assertion..... 
1. g : EuclideanPlane
2. p : Length
3. q : Length
4. ¬p < q
5. ¬q ≤ p
⊢ False
BY
{ (UseWitness ⌜⋅⌝⋅ THEN DVar `p' THEN DVar `q' THEN Assert ⌜False⌝⋅ THEN Auto) }

1
.....assertion..... 
1. g : EuclideanPlane
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
15. ¬q ≤ p
⊢ False

---

Latex:

---

Latex:
.....assertion..... 
1.  g  :  EuclideanPlane
2.  p  :  Length
3.  q  :  Length
4.  \mneg{}p  <  q
5.  \mneg{}q  \mleq{}  p
\mvdash{}  False


By

---

Latex:
(UseWitness  \mkleeneopen{}\mcdot{}\mkleeneclose{}\mcdot{}  THEN  DVar  `p'  THEN  DVar  `q'  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index