---

Step * of Lemma not-lt-or

∀g:EuclideanPlane. ∀p,q:Length.  (¬¬(p < q ∨ q < p ∨ (p = q ∈ Length)))
BY
{ (Auto THEN (D 0 THENA Auto)) }

1
1. g : EuclideanPlane
2. p : Length
3. q : Length
4. ¬(p < q ∨ q < p ∨ (p = q ∈ Length))
⊢ False

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}p,q:Length.    (\mneg{}\mneg{}(p  <  q  \mvee{}  q  <  p  \mvee{}  (p  =  q)))


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto))

---

Home Index