---

Step * of Lemma geo-le-null-segment

∀e:BasicGeometry. ∀[p:Length]. ∀[a:Point].  uiff(p ≤ |aa|;p = |aa| ∈ Length)
BY
{ ((Intros
    THEN (Assert {p:Point| O_X_p}  ⊆r Length BY
                Auto)
    THEN (Unhide THENA Auto)
    THEN D 0
    THEN Intro
    THEN (Unhide THENA Auto)
    THEN Try (((RWO "-1" 0 THEN Auto) THEN BLemma `geo-le_weakening` THEN Auto)))
   THEN (Assert X ∈ Length BY
               (SubsumeC ⌜{p:Point| O_X_p} ⌝⋅ THEN Auto))
   THEN RWO "geo-length-null-segment" 0
   THEN Auto) }

1
1. e : BasicGeometry
2. p : Length
3. a : Point
4. {p:Point| O_X_p}  ⊆r Length
5. p ≤ |aa|
6. X ∈ Length
⊢ p = X ∈ Length

---

Latex:

---

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


By

---

Latex:
((Intros
    THEN  (Assert  \{p:Point|  O\_X\_p\}    \msubseteq{}r  Length  BY
                            Auto)
    THEN  (Unhide  THENA  Auto)
    THEN  D  0
    THEN  Intro
    THEN  (Unhide  THENA  Auto)
    THEN  Try  (((RWO  "-1"  0  THEN  Auto)  THEN  BLemma  `geo-le\_weakening`  THEN  Auto)))
  THEN  (Assert  X  \mmember{}  Length  BY
                          (SubsumeC  \mkleeneopen{}\{p:Point|  O\_X\_p\}  \mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  RWO  "geo-length-null-segment"  0
  THEN  Auto)

---

Home Index