---

Step * of Lemma geo-lt-null-segment

∀e:BasicGeometry. ∀[p:Length]. ∀[a:Point].  uiff(p < |aa|;False)
BY
{ (Auto
   THEN D -1
   THEN ExRepD
   THEN (RWO "geo-le-null-segment" (-1) THENA Auto)
   THEN (RWO "geo-length-null-segment" (-1) THENA Auto)
   THEN Fold `geo-zero-length` (-1)
   THEN (RWO  "geo-add-length-is-zero" (-1) THENA Auto)) }

1
1. e : BasicGeometry
2. p : Length
3. a : Point
4. a@0 : Point
5. b : Point
6. a@0 ≠ b
7. (p = 0 ∈ Length) ∧ (|a@0b| = 0 ∈ Length)
⊢ False

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}[p:Length].  \mforall{}[a:Point].    uiff(p  <  |aa|;False)


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  ExRepD
  THEN  (RWO  "geo-le-null-segment"  (-1)  THENA  Auto)
  THEN  (RWO  "geo-length-null-segment"  (-1)  THENA  Auto)
  THEN  Fold  `geo-zero-length`  (-1)
  THEN  (RWO    "geo-add-length-is-zero"  (-1)  THENA  Auto))

---

Home Index