---

Step * of Lemma eu-between-eq-same

∀[e:EuclideanPlane]. ∀[a,b:Point].  a = b ∈ Point supposing a_b_a
BY
{ Auto }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. a_b_a
⊢ a = b ∈ Point

---

Latex:

---

Latex:
\mforall{}[e:EuclideanPlane].  \mforall{}[a,b:Point].    a  =  b  supposing  a\_b\_a


By

---

Latex:
Auto

---

Home Index