---

Step * 1 1 of Lemma mk-complete-pgeo_wf


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

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

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

---

Latex:

---

Latex:

1.  [pg]  :  ProjectivePlaneStructure
2.  [p]  :  Point
\mvdash{}  pg["non-trivial"  :=  <p,  \mlambda{}x.x>]  \mmember{}  ProjectivePlaneStructure
    "non-trivial":\mexists{}p:Point.  p  \mequiv{}  p


By

---

Latex:
RecordPlusTypeCD

---

Home Index