---

Step * of Lemma sq_stable-pgeo-axioms-if

∀[g:ProjGeomPrimitives]. ((∀a:Point. ∀L:Line.  SqStable(a ≠ L)) ⇒ SqStable(BasicProjectiveGeometryAxioms(g)))
BY
{ ((UnivCD THENA Auto⋅) THEN RepUR ``basic-pgeo-axioms pgeo-peq pgeo-leq pgeo-incident `` 0 THEN Auto⋅) }

---

Latex:

---

Latex:
\mforall{}[g:ProjGeomPrimitives]
    ((\mforall{}a:Point.  \mforall{}L:Line.    SqStable(a  \mneq{}  L))  {}\mRightarrow{}  SqStable(BasicProjectiveGeometryAxioms(g)))


By

---

Latex:
((UnivCD  THENA  Auto\mcdot{})
  THEN  RepUR  ``basic-pgeo-axioms  pgeo-peq  pgeo-leq  pgeo-incident  ``  0
  THEN  Auto\mcdot{})

---

Home Index