---

Step * of Lemma pp-sep_wf

∀[eu:EuclideanParPlane]. ∀[p:Point + Line]. ∀[l:Line?].  (pp-sep(eu;p;l) ∈ ℙ)
BY
{ (Auto THEN D -2 THEN D -1 THEN RepUR ``pp-sep`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[eu:EuclideanParPlane].  \mforall{}[p:Point  +  Line].  \mforall{}[l:Line?].    (pp-sep(eu;p;l)  \mmember{}  \mBbbP{})


By

---

Latex:
(Auto  THEN  D  -2  THEN  D  -1  THEN  RepUR  ``pp-sep``  0  THEN  Auto)

---

Home Index