---

Step * of Lemma geo-length-between-property

∀e:BasicGeometry. ∀p,q:{p:Point| O_X_p} . ∀a,b,c,d:Point.
  (X_p_q ⇒ (p = |ab| ∈ Length) ⇒ (q = |cd| ∈ Length) ⇒ X_|ab|_|cd|)
BY
{ ((UnivCD THENA Auto)
   THEN (Assert |ab| ≤ |cd| BY
               ((Assert p ≤ q BY
                       (FLemma `geo-le-iff-between-points` [8] THEN Auto))
                THEN D 0
                THEN InstConcl [⌜p⌝;⌜q⌝]⋅
                THEN Auto))
   THEN FLemma `geo-le-iff-between-points` [-1]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}p,q:\{p:Point|  O\_X\_p\}  .  \mforall{}a,b,c,d:Point.
    (X\_p\_q  {}\mRightarrow{}  (p  =  |ab|)  {}\mRightarrow{}  (q  =  |cd|)  {}\mRightarrow{}  X\_|ab|\_|cd|)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Assert  |ab|  \mleq{}  |cd|  BY
                          ((Assert  p  \mleq{}  q  BY
                                          (FLemma  `geo-le-iff-between-points`  [8]  THEN  Auto))
                            THEN  D  0
                            THEN  InstConcl  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}
                            THEN  Auto))
  THEN  FLemma  `geo-le-iff-between-points`  [-1]
  THEN  Auto)

---

Home Index