---

Step * of Lemma Euclid-Prop20_cycle

∀e:EuclideanPlane. ∀a,b,c:Point.  (a # bc ⇒ (|bc| < |ba| + |ac| ∧ |ac| < |ba| + |bc| ∧ |ba| < |ac| + |bc|))
BY
{ EAuto 1 }

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

2
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|

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c:Point.
    (a  \#  bc  {}\mRightarrow{}  (|bc|  <  |ba|  +  |ac|  \mwedge{}  |ac|  <  |ba|  +  |bc|  \mwedge{}  |ba|  <  |ac|  +  |bc|))


By

---

Latex:
EAuto  1

---

Home Index