---

Step * of Lemma mk-complete-pgeo_wf

No Annotations
∀[pg:ProjectivePlaneStructure]. ∀[p:Point].  (mk-complete-pgeo(pg;p) ∈ ProjectivePlaneStructureComplete)
BY
{ Intros }

1
1. [pg] : ProjectivePlaneStructure
2. [p] : Point
⊢ mk-complete-pgeo(pg;p) ∈ ProjectivePlaneStructureComplete

---

Latex:

---

Latex:
No  Annotations
\mforall{}[pg:ProjectivePlaneStructure].  \mforall{}[p:Point].
    (mk-complete-pgeo(pg;p)  \mmember{}  ProjectivePlaneStructureComplete)


By

---

Latex:
Intros

---

Home Index