---

Step * 1 of Lemma midpoint-construction_wf


1. e : EuclideanPlane
2. a : Point
3. b : {b:Point| a ≠ b} 
⊢ TERMOF{Euclid-midpoint-1:o, 1:l, i:l} e a b ∈ ∃d:Point [a=d=b]
BY
{ Auto }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  \{b:Point|  a  \mneq{}  b\} 
\mvdash{}  TERMOF\{Euclid-midpoint-1:o,  1:l,  i:l\}  e  a  b  \mmember{}  \mexists{}d:Point  [a=d=b]


By

---

Latex:
Auto

---

Home Index