---

Step * of Lemma midpoint-construction_wf

∀e:EuclideanPlane. ∀a:Point. ∀b:{b:Point| a ≠ b} .  (Mid(a;b) ∈ {d:Point| a=d=b} )
BY
{ ((Auto THEN Fold `sq_exists` 0)
   THEN (Subst' Mid(a;b) ~ TERMOF{Euclid-midpoint-1:o, 1:l, i:l} e a b 0
         THENA (RW (AddrC [2] (TagC (mk_tag_term 100))) 0 THEN Computation THEN Auto THEN Computation)
         )
   ) }

1
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]

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a:Point.  \mforall{}b:\{b:Point|  a  \mneq{}  b\}  .    (Mid(a;b)  \mmember{}  \{d:Point|  a=d=b\}  )


By

---

Latex:
((Auto  THEN  Fold  `sq\_exists`  0)
  THEN  (Subst'  Mid(a;b)  \msim{}  TERMOF\{Euclid-midpoint-1:o,  1:l,  i:l\}  e  a  b  0
              THENA  (RW  (AddrC  [2]  (TagC  (mk\_tag\_term  100)))  0  THEN  Computation  THEN  Auto  THEN  Computation)
              )
  )

---

Home Index