---

Step * 1 of Lemma mk-complete-pgeo_wf


1. [pg] : ProjectivePlaneStructure
2. [p] : Point
⊢ mk-complete-pgeo(pg;p) ∈ ProjectivePlaneStructureComplete
BY
{ Unfolds ``projective-plane-structure-complete mk-complete-pgeo`` 0 }

1
1. [pg] : ProjectivePlaneStructure
2. [p] : Point
⊢ pg["non-trivial" := <p, λx.x>] ∈ ProjectivePlaneStructure
  "non-trivial":∃p:Point. p ≡ p

---

Latex:

---

Latex:

1.  [pg]  :  ProjectivePlaneStructure
2.  [p]  :  Point
\mvdash{}  mk-complete-pgeo(pg;p)  \mmember{}  ProjectivePlaneStructureComplete


By

---

Latex:
Unfolds  ``projective-plane-structure-complete  mk-complete-pgeo``  0

---

Home Index