---

Step * of Lemma point-exists-axiom_wf

No Annotations
∀[g:ProjectivePlaneStructureComplete]. (point-exists-axiom(g) ∈ ∃p:Point. p ≡ p)
BY
{ (ProveWfLemma THEN D 1 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[g:ProjectivePlaneStructureComplete].  (point-exists-axiom(g)  \mmember{}  \mexists{}p:Point.  p  \mequiv{}  p)


By

---

Latex:
(ProveWfLemma  THEN  D  1  THEN  Auto)

---

Home Index