---

Step * of Lemma eu-line-circle_wf

∀[e:EuclideanStructure]. ∀[a,b:Point]. ∀[x:{x:Point| a_x_b} ]. ∀[y:{y:Point| a_b_y} ]. ∀[p:{p:Point| ap=ax} ].
∀[q:{q:Point| aq=ay ∧ (¬(q = p ∈ Point))} ].
  (intersect pq (at radius xy) with Oab  ∈ Point × Point)
BY
{ (ProveWfLemma THEN All (Unfolds ``eu-point eu-congruent eu-between-eq``)⋅ THEN DRecord 1 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[e:EuclideanStructure].  \mforall{}[a,b:Point].  \mforall{}[x:\{x:Point|  a\_x\_b\}  ].  \mforall{}[y:\{y:Point|  a\_b\_y\}  ].  \mforall{}[p:\{p:Point|\000C 
                                                                                                                                                                                    ap=ax\}  ].
\mforall{}[q:\{q:Point|  aq=ay  \mwedge{}  (\mneg{}(q  =  p))\}  ].
    (intersect  pq  (at  radius  xy)  with  Oab    \mmember{}  Point  \mtimes{}  Point)


By

---

Latex:
(ProveWfLemma  THEN  All  (Unfolds  ``eu-point  eu-congruent  eu-between-eq``)\mcdot{}  THEN  DRecord  1  THEN  Auto)

---

Home Index