---

Step * of Lemma geo-le_weakening

∀[e:BasicGeometry]. ∀[p,q:Length].  p ≤ q supposing p = q ∈ Length
BY
{ ((Intros THEN (Unhide THENA Auto))
   THEN (HypSubst' -1 0 THENA Auto)
   THEN All Thin
   THEN (Assert {p:Point| O_X_p}  ⊆r Length BY
               Auto)
   THEN UseWitness ⌜Ax⌝⋅
   THEN D 2
   THEN Fold `member` 0
   THEN BLemma `geo-le_witness` 
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[e:BasicGeometry].  \mforall{}[p,q:Length].    p  \mleq{}  q  supposing  p  =  q


By

---

Latex:
((Intros  THEN  (Unhide  THENA  Auto))
  THEN  (HypSubst'  -1  0  THENA  Auto)
  THEN  All  Thin
  THEN  (Assert  \{p:Point|  O\_X\_p\}    \msubseteq{}r  Length  BY
                          Auto)
  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
  THEN  D  2
  THEN  Fold  `member`  0
  THEN  BLemma  `geo-le\_witness` 
  THEN  Auto)

---

Home Index