---

Step * of Lemma triangle-inequality-for-colinear

∀[e:EuclideanPlane]. ∀[a,b,c:Point].  (Colinear(b;a;c) ⇒ |ac| ≤ |ab| + |bc|)
BY
{ (Auto
   THEN gSimpleColinearCases (-1)
   THEN FLemma `geo-add-length-between` [-1]
   THEN Auto
   THEN Try ((RWO "-1" 0 THEN Auto))) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. Colinear(b;a;c)
6. b_a_c
7. |bc| = |ba| + |ac| ∈ Length
⊢ |ac| ≤ |ab| + |ba| + |ac|

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. Colinear(b;a;c)
6. a_c_b
7. |ab| = |ac| + |cb| ∈ Length
⊢ |ac| ≤ |ac| + |cb| + |bc|

3
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. Colinear(b;a;c)
6. c_b_a
7. |ca| = |cb| + |ba| ∈ Length
⊢ |ac| ≤ |ab| + |bc|

---

Latex:

---

Latex:
\mforall{}[e:EuclideanPlane].  \mforall{}[a,b,c:Point].    (Colinear(b;a;c)  {}\mRightarrow{}  |ac|  \mleq{}  |ab|  +  |bc|)


By

---

Latex:
(Auto
  THEN  gSimpleColinearCases  (-1)
  THEN  FLemma  `geo-add-length-between`  [-1]
  THEN  Auto
  THEN  Try  ((RWO  "-1"  0  THEN  Auto)))

---

Home Index