---

Step * 1 of Lemma op-geo-left-axioms


1. g : EuclideanPlaneStructure
2. BasicGeometryAxioms(g)
3. g ∈ EuclideanPlane
⊢ geo-left-axioms(g)
BY
{ (((D -2 THEN D 0 THEN GenRepD) THEN Auto) THEN InstHyp [⌜a⌝;⌜b⌝;⌜x⌝;⌜y⌝;⌜z⌝] (13)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  EuclideanPlaneStructure
2.  BasicGeometryAxioms(g)
3.  g  \mmember{}  EuclideanPlane
\mvdash{}  geo-left-axioms(g)


By

---

Latex:
(((D  -2  THEN  D  0  THEN  GenRepD)  THEN  Auto)  THEN  InstHyp  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]  (13)\mcdot{}  THEN  Auto)

---

Home Index