---

Step * of Lemma r2-eu_wf

No Annotations
EuclideanPlane(ℝ^2) ∈ EuclideanPlane
BY
{ (Unfold `r2-eu` 0
   THEN BLemma `mk-eu_wf2`
   THEN Try (BLemma `r2-eu-prim_wf`)
   THEN Try (BLemma `r2-basic-geo-axioms`)
   THEN UnfoldGeoAbbreviations 0
   THEN RepUR ``r2-eu-prim mk-eu-prim`` 0
   THEN Try (QuickAuto)) }

---

Latex:

---

Latex:
No  Annotations
EuclideanPlane(\mBbbR{}\^{}2)  \mmember{}  EuclideanPlane


By

---

Latex:
(Unfold  `r2-eu`  0
  THEN  BLemma  `mk-eu\_wf2`
  THEN  Try  (BLemma  `r2-eu-prim\_wf`)
  THEN  Try  (BLemma  `r2-basic-geo-axioms`)
  THEN  UnfoldGeoAbbreviations  0
  THEN  RepUR  ``r2-eu-prim  mk-eu-prim``  0
  THEN  Try  (QuickAuto))

---

Home Index