---

Step * of Lemma pgeo-non-trivial

∀g:ProjectivePlaneStructureComplete. ∃p:Point. p ≡ p
BY
{ (Auto THEN UseWitness ⌜point-exists-axiom(g)⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g:ProjectivePlaneStructureComplete.  \mexists{}p:Point.  p  \mequiv{}  p


By

---

Latex:
(Auto  THEN  UseWitness  \mkleeneopen{}point-exists-axiom(g)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index