---

Step * 1 of Lemma Euclid-Prop20_cycle


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. |bc| < |ba| + |ac|
⊢ |ac| < |ba| + |bc|
BY
{ ((FLemma `lsep-all-sym` [-2] THEN Auto) THEN FLemma `Euclid-Prop20` [-2]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a  \#  bc
6.  |bc|  <  |ba|  +  |ac|
\mvdash{}  |ac|  <  |ba|  +  |bc|


By

---

Latex:
((FLemma  `lsep-all-sym`  [-2]  THEN  Auto)  THEN  FLemma  `Euclid-Prop20`  [-2]\mcdot{}  THEN  Auto)

---

Home Index