---

Step * of Lemma P_point-sep_wf

∀[eu:EuclideanParPlane]. ∀P,Q:P_point(eu).  (P_point-sep(eu;P;Q) ∈ ℙ)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[eu:EuclideanParPlane].  \mforall{}P,Q:P\_point(eu).    (P\_point-sep(eu;P;Q)  \mmember{}  \mBbbP{})


By

---

Latex:
ProveWfLemma

---

Home Index