---

Step * 1 1 2 of Lemma mk-complete-pgeo_wf


1. pg : ProjectivePlaneStructure
2. p : Point
⊢ pg["non-trivial" := <p, λx.x>]."non-trivial" ∈ ∃p@0:Point. p@0 ≡ p@0
BY
{ (UnfoldpGeoAbbreviations 0 THEN FoldpGeoAbbreviations 0) }

1
1. pg : ProjectivePlaneStructure
2. p : Point
⊢ <p, λx.x> ∈ ∃p@0:Point. p@0 ≡ p@0

---

Latex:

---

Latex:

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


By

---

Latex:
(UnfoldpGeoAbbreviations  0  THEN  FoldpGeoAbbreviations  0)

---

Home Index