---

Step * of Lemma op-geo-left-axioms

No Annotations
∀g:OrientedPlane. geo-left-axioms(g)
BY
{ (((D 0 THENA Auto) THEN (Assert g ∈ EuclideanPlane BY Auto) THEN D 1 THEN Unhide THEN Auto)
   THEN Try ((Unhide THEN Auto))
   ) }

1
1. g : EuclideanPlaneStructure
2. BasicGeometryAxioms(g)
3. g ∈ EuclideanPlane
⊢ geo-left-axioms(g)

---

Latex:

---

Latex:
No  Annotations
\mforall{}g:OrientedPlane.  geo-left-axioms(g)


By

---

Latex:
(((D  0  THENA  Auto)  THEN  (Assert  g  \mmember{}  EuclideanPlane  BY  Auto)  THEN  D  1  THEN  Unhide  THEN  Auto)
  THEN  Try  ((Unhide  THEN  Auto))
  )

---

Home Index