---

Step * of Lemma ip-between-sep

∀rv:InnerProductSpace. ∀a,c:Point.  ∀[b:Point]. (a # c) supposing (a # b and a_b_c)
BY
{ (Auto THEN Unhide THEN Auto THEN (FLemma `ip-dist-between` [-2] THENA Auto)) }

1
1. rv : InnerProductSpace
2. a : Point
3. c : Point
4. b : Point
5. a_b_c
6. a # b
7. ||a - c|| = (||a - b|| + ||b - c||)
⊢ a # c

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}a,c:Point.    \mforall{}[b:Point].  (a  \#  c)  supposing  (a  \#  b  and  a\_b\_c)


By

---

Latex:
(Auto  THEN  Unhide  THEN  Auto  THEN  (FLemma  `ip-dist-between`  [-2]  THENA  Auto))

---

Home Index