---

Step * of Lemma P_point-line-sep_wf

No Annotations
∀[eu:EuclideanParPlane]. ∀P:P_point(eu). ∀n:P_line(eu).  (P_point-line-sep(eu;P;n) ∈ ℙ)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[eu:EuclideanParPlane].  \mforall{}P:P\_point(eu).  \mforall{}n:P\_line(eu).    (P\_point-line-sep(eu;P;n)  \mmember{}  \mBbbP{})


By

---

Latex:
ProveWfLemma

---

Home Index