---

Step * of Lemma pgeo-dual_wf

∀[pg:ProjectivePlaneStructure]. (pg* ∈ ProjectivePlaneStructure)
BY
{ (Auto
   THEN (Assert pg ∈ ProjectivePlaneStructure BY
               Auto)
   THEN (D 1 THENA Auto)
   THEN (Unfold `pgeo-dual` 0 THEN MemCD)
   THEN Try (QuickAuto)
   THEN UnfoldpGeoAbbreviations  0
   THEN FoldpGeoAbbreviations  0
   THEN Try (Trivial)
   THEN Try ((All UnfoldpGeoAbbreviations ⋅ THEN Trivial))) }

---

Latex:

---

Latex:
\mforall{}[pg:ProjectivePlaneStructure].  (pg*  \mmember{}  ProjectivePlaneStructure)


By

---

Latex:
(Auto
  THEN  (Assert  pg  \mmember{}  ProjectivePlaneStructure  BY
                          Auto)
  THEN  (D  1  THENA  Auto)
  THEN  (Unfold  `pgeo-dual`  0  THEN  MemCD)
  THEN  Try  (QuickAuto)
  THEN  UnfoldpGeoAbbreviations    0
  THEN  FoldpGeoAbbreviations    0
  THEN  Try  (Trivial)
  THEN  Try  ((All  UnfoldpGeoAbbreviations  \mcdot{}  THEN  Trivial)))

---

Home Index