---

Step * 1 of Lemma eu-add-length-between


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a_b_c
⊢ |ac| = |ab| + |bc| ∈ Point
BY
{ (Unfold `eu-add-length` 0 THEN (Assert ¬(O = X ∈ Point) BY Auto)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a_b_c
6. ¬(O = X ∈ Point)
⊢ |ac| = (extend O|ab| by X|bc|) ∈ Point

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a\_b\_c
\mvdash{}  |ac|  =  |ab|  +  |bc|


By

---

Latex:
(Unfold  `eu-add-length`  0  THEN  (Assert  \mneg{}(O  =  X)  BY  Auto))

---

Home Index