---

Step * 1 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
⊢ (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)
BY
{ (Unhide THENA Auto) }

1
1. e : EuclideanStructure@i'
2. 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{}  (middle(a;b;c)  =  middle(a;b;c))  \mwedge{}  amiddle(a;b;c)=bmiddle(a;b;c)  \mwedge{}  amiddle(a;b;c)=cmiddle(a;b;c)


By

---

Latex:
(Unhide  THENA  Auto)

---

Home Index