---

Step * 3 of Lemma triangle-inequality-for-colinear


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|
BY
{ ((RWO "geo-length-flip" (-1) THENA Auto) THEN (RWO  "-1" 0 THENA Auto)) }

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

---

Latex:

---

Latex:

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|
\mvdash{}  |ac|  \mleq{}  |ab|  +  |bc|


By

---

Latex:
((RWO  "geo-length-flip"  (-1)  THENA  Auto)  THEN  (RWO    "-1"  0  THENA  Auto))

---

Home Index