---

Step * of Lemma dist-lemma-lt-2

∀g:EuclideanPlane. ∀a,b,e,f:Point.  (D(a;b;b;b;e;f) ⇒ |ef| < |ab|)
BY
{ (Auto
   THEN (FLemma `dist-lemma-lt` [-1] THENA Auto)
   THEN ((Subst' |ab| + |bb| = |ab| ∈ Length (-1) THEN Auto)
         THENA (InstLemma `geo-add-length-zero` [⌜g⌝;⌜|ab|⌝]⋅ THEN Auto)
         )) }

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,e,f:Point.    (D(a;b;b;b;e;f)  {}\mRightarrow{}  |ef|  <  |ab|)


By

---

Latex:
(Auto
  THEN  (FLemma  `dist-lemma-lt`  [-1]  THENA  Auto)
  THEN  ((Subst'  |ab|  +  |bb|  =  |ab|  (-1)  THEN  Auto)
              THENA  (InstLemma  `geo-add-length-zero`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}|ab|\mkleeneclose{}]\mcdot{}  THEN  Auto)
              ))

---

Home Index