---

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


1. pg : ProjectivePlaneStructure
2. p : Point
⊢ <p, λx.x> ∈ ∃p@0:Point. p@0 ≡ p@0
BY
{ (MemCD THEN Auto) }

1
.....subterm..... T:t
2:n
1. pg : ProjectivePlaneStructure
2. p : Point
⊢ λx.x ∈ p ≡ p

---

Latex:

---

Latex:

1.  pg  :  ProjectivePlaneStructure
2.  p  :  Point
\mvdash{}  <p,  \mlambda{}x.x>  \mmember{}  \mexists{}p@0:Point.  p@0  \mequiv{}  p@0


By

---

Latex:
(MemCD  THEN  Auto)

---

Home Index