---

Step * of Lemma dist-lemma-le

∀g:EuclideanPlane. ∀a,b,c,d,e,f:Point.  (D(a;b;c;d;e;f) ⇒ |ef| ≤ |ab| + |cd|)
BY
{ (Auto
   THEN Unfold `dist` -1
   THEN ExRepD
   THEN (Assert ⌜|a'u| ≤ |a'b'| + |b'c'|⌝⋅ THENM Auto)
   THEN RWO "geo-add-length-between-iff" 12
   THEN Auto
   THEN FLemma `geo-le-from-be` [13]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,d,e,f:Point.    (D(a;b;c;d;e;f)  {}\mRightarrow{}  |ef|  \mleq{}  |ab|  +  |cd|)


By

---

Latex:
(Auto
  THEN  Unfold  `dist`  -1
  THEN  ExRepD
  THEN  (Assert  \mkleeneopen{}|a'u|  \mleq{}  |a'b'|  +  |b'c'|\mkleeneclose{}\mcdot{}  THENM  Auto)
  THEN  RWO  "geo-add-length-between-iff"  12
  THEN  Auto
  THEN  FLemma  `geo-le-from-be`  [13]\mcdot{}
  THEN  Auto)

---

Home Index