---

Step * of Lemma pgeo-dual_wf2

∀[pg:BasicProjectivePlane]. (pg* ∈ BasicProjectivePlane)
BY
{ (((Auto THEN D -1 THEN MemTypeCD THEN Auto)
    THEN ParallelLast
    THEN ExRepD
    THEN SplitAndConcl
    THEN All (UnfoldpGeoAbbreviations)
    THEN (Trivial ORELSE (All (FoldpGeoAbbreviations) THEN Auto)))
   THEN InstHyp [⌜q⌝;⌜p⌝;⌜l⌝;⌜m⌝] 2⋅
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(((Auto  THEN  D  -1  THEN  MemTypeCD  THEN  Auto)
    THEN  ParallelLast
    THEN  ExRepD
    THEN  SplitAndConcl
    THEN  All  (UnfoldpGeoAbbreviations)
    THEN  (Trivial  ORELSE  (All  (FoldpGeoAbbreviations)  THEN  Auto)))
  THEN  InstHyp  [\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]  2\mcdot{}
  THEN  Auto)

---

Home Index