---

Step * of Lemma oriented-plane-axioms

∀g:OrientedPlane. ∀P:OrientedPlane ⟶ ℙ.
  ((∀g:OrientedPlane. (BasicGeometryAxioms(g) ⇒ geo-left-axioms(g) ⇒ P[g])) ⇒ P[g])
BY
{ (Auto THEN BHyp -1  THEN Auto THEN D 1 THEN Unhide THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g:OrientedPlane.  \mforall{}P:OrientedPlane  {}\mrightarrow{}  \mBbbP{}.
    ((\mforall{}g:OrientedPlane.  (BasicGeometryAxioms(g)  {}\mRightarrow{}  geo-left-axioms(g)  {}\mRightarrow{}  P[g]))  {}\mRightarrow{}  P[g])


By

---

Latex:
(Auto  THEN  BHyp  -1    THEN  Auto  THEN  D  1  THEN  Unhide  THEN  Auto)

---

Home Index