---

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

No Annotations
∀e:BasicGeometry. ∀[a,b,c:Point].  uiff(B(abc);|ac| = |ab| + |bc| ∈ Length)
BY
{ Auto }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. |ac| = |ab| + |bc| ∈ Length
⊢ B(abc)

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:BasicGeometry.  \mforall{}[a,b,c:Point].    uiff(B(abc);|ac|  =  |ab|  +  |bc|)


By

---

Latex:
Auto

---

Home Index