---

Step * of Lemma eu-pp-prim_wf

∀[eu:EuclideanParPlane]. (pp(eu) ∈ ProjGeomPrimitives)
BY
{ (Auto THEN Unfold `eu-pp-prim` 0 THEN MemCD THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[eu:EuclideanParPlane].  (pp(eu)  \mmember{}  ProjGeomPrimitives)


By

---

Latex:
(Auto  THEN  Unfold  `eu-pp-prim`  0  THEN  MemCD  THEN  Auto)

---

Home Index