---

Step * of Lemma geo-lt-null-segment2

∀e:BasicGeometry. ∀[p:Length]. ∀[a,b:Point].  (False) supposing (a ≡ b and p < |ab|)
BY
{ Auto }

1
1. e : BasicGeometry
2. p : Length
3. a : Point
4. b : Point
5. p < |ab|
6. a ≡ b
⊢ False

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}[p:Length].  \mforall{}[a,b:Point].    (False)  supposing  (a  \mequiv{}  b  and  p  <  |ab|)


By

---

Latex:
Auto

---

Home Index