---

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

.....subterm..... T:t
2:n
1. pg : ProjectivePlaneStructure
2. p : Point
⊢ λx.x ∈ p ≡ p
BY
{ (Unfold `pgeo-peq` 0 THEN Unfold `not` 0 THEN Auto) }

1
1. pg : ProjectivePlaneStructure
2. p : Point
3. x : p ≠ p@i
⊢ x ∈ False

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  pg  :  ProjectivePlaneStructure
2.  p  :  Point
\mvdash{}  \mlambda{}x.x  \mmember{}  p  \mequiv{}  p


By

---

Latex:
(Unfold  `pgeo-peq`  0  THEN  Unfold  `not`  0  THEN  Auto)

---

Home Index