---

Step * of Lemma eu-extend-exists

∀e:EuclideanPlane. ∀q:Point. ∀a:{a:Point| ¬(q = a ∈ Point)} . ∀b,c:Point.  ∃x:Point. (q_a_x ∧ ax=bc)
BY
{ (Auto THEN With ⌜(extend qa by bc)⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}q:Point.  \mforall{}a:\{a:Point|  \mneg{}(q  =  a)\}  .  \mforall{}b,c:Point.    \mexists{}x:Point.  (q\_a\_x  \mwedge{}  ax=bc)


By

---

Latex:
(Auto  THEN  With  \mkleeneopen{}(extend  qa  by  bc)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index