---

Step * of Lemma eu-exists-middle

∀e:EuclideanPlane. ∀a,b:Point. ∀c:{p:Point| ¬Colinear(a;b;p)} .  ∃m:Point. ((m = middle(a;b;c) ∈ Point) ∧ am=bm ∧ am=cm)
BY
{ Auto
THEN D 1 }

1
1. e : EuclideanStructure@i'
2. [%1] : euclidean-axioms(e)@i'
3. a : Point@i
4. b : Point@i
5. c : {p:Point| ¬Colinear(a;b;p)} @i
⊢ ∃m:Point. ((m = middle(a;b;c) ∈ Point) ∧ am=bm ∧ am=cm)

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b:Point.  \mforall{}c:\{p:Point|  \mneg{}Colinear(a;b;p)\}  .
    \mexists{}m:Point.  ((m  =  middle(a;b;c))  \mwedge{}  am=bm  \mwedge{}  am=cm)


By

---

Latex:
Auto
THEN  D  1

---

Home Index