---

Step * of Lemma ip-between-rless

∀rv:InnerProductSpace. ∀a,b,c:Point.  (a_b_c ⇒ b # c ⇒ (||a - b|| < ||a - c||))
BY
{ (Auto
   THEN (FLemma `ip-dist-between` [5] THENA Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN (Assert r0 < ||b - c|| BY
               EAuto 1⋅)
   THEN nRAdd ⌜||a - b||⌝ (-1)⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}a,b,c:Point.    (a\_b\_c  {}\mRightarrow{}  b  \#  c  {}\mRightarrow{}  (||a  -  b||  <  ||a  -  c||))


By

---

Latex:
(Auto
  THEN  (FLemma  `ip-dist-between`  [5]  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  (Assert  r0  <  ||b  -  c||  BY
                          EAuto  1\mcdot{})
  THEN  nRAdd  \mkleeneopen{}||a  -  b||\mkleeneclose{}  (-1)\mcdot{}
  THEN  Auto)

---

Home Index