---

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


1. pg : ProjectivePlaneStructure
2. p : Point
3. x : p ≠ p@i
⊢ x ∈ False
BY
{ (RepeatFor 2 (D -1) THEN D -2 THEN Auto) }

---

Latex:

---

Latex:

1.  pg  :  ProjectivePlaneStructure
2.  p  :  Point
3.  x  :  p  \mneq{}  p@i
\mvdash{}  x  \mmember{}  False


By

---

Latex:
(RepeatFor  2  (D  -1)  THEN  D  -2  THEN  Auto)

---

Home Index