---

Step * 1 of Lemma eu-exists-middle


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)
BY
{ (InstConcl [⌜middle(a;b;c)⌝]⋅ THENA Auto) }

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
⊢ (middle(a;b;c) = middle(a;b;c) ∈ Point) ∧ amiddle(a;b;c)=bmiddle(a;b;c) ∧ amiddle(a;b;c)=cmiddle(a;b;c)

---

Latex:

---

Latex:

1.  e  :  EuclideanStructure@i'
2.  [\%1]  :  euclidean-axioms(e)@i'
3.  a  :  Point@i
4.  b  :  Point@i
5.  c  :  \{p:Point|  \mneg{}Colinear(a;b;p)\}  @i
\mvdash{}  \mexists{}m:Point.  ((m  =  middle(a;b;c))  \mwedge{}  am=bm  \mwedge{}  am=cm)


By

---

Latex:
(InstConcl  [\mkleeneopen{}middle(a;b;c)\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index