---

Step * 1 of Lemma dual-plane_wf


1. pg : ProjectivePlaneStructureComplete
2. BasicProjectiveGeometryAxioms(pg)
3. triangle-axiom1(pg)
4. triangle-axiom2(pg)
⊢ dual-plane(pg) ∈ ProjectivePlaneStructureComplete
BY
{ ProveWfLemma }

1
1. pg : ProjectivePlaneStructureComplete
2. BasicProjectiveGeometryAxioms(pg)
3. triangle-axiom1(pg)
4. triangle-axiom2(pg)
⊢ let p,_ = pg "non-trivial" 
  in let l,_ = pg "three-lines" p 
     in l ∈ Line

---

Latex:

---

Latex:

1.  pg  :  ProjectivePlaneStructureComplete
2.  BasicProjectiveGeometryAxioms(pg)
3.  triangle-axiom1(pg)
4.  triangle-axiom2(pg)
\mvdash{}  dual-plane(pg)  \mmember{}  ProjectivePlaneStructureComplete


By

---

Latex:
ProveWfLemma

---

Home Index