---

Step * 2 of Lemma Euclid-Prop20_cycle


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index