---

Step * 2 1 of Lemma not-geo-lt


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

1
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. q ≤ p
15. p < q
⊢ ⋅ = ⋅ ∈ False

---

Latex:

---

Latex:

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


By

---

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

---

Home Index