---

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

∀e:EuclideanPlane. ∀[a,b,c:Point].  uiff(a_b_c;|ac| = |ab| + |bc| ∈ {p:Point| O_X_p} )
BY
{ Auto }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a_b_c
⊢ |ac| = |ab| + |bc| ∈ {p:Point| O_X_p} 

2
1. e : EuclideanPlane
2. [a] : Point
3. [b] : Point
4. [c] : Point
5. |ac| = |ab| + |bc| ∈ {p:Point| O_X_p} 
⊢ a_b_c

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}[a,b,c:Point].    uiff(a\_b\_c;|ac|  =  |ab|  +  |bc|)


By

---

Latex:
Auto

---

Home Index