---

Step * of Lemma mk-s-subgroup_wf

∀[sg:s-Group]. ∀[P:Point ⟶ ℙ].  mk-s-subgroup(sg;x.P[x]) ∈ s-Group supposing sg-subgroup(sg;x.P[x])
BY
{ ((Auto THEN D -1 THEN ExRepD)
   THEN Unfold `mk-s-subgroup` 0
   THEN MemCD
   THEN (All  (RWO "set-ss-point set-ss-eq set-ss-sep") THENA Auto)
   THEN ((Reduce 0
          THEN (Assert sg ∈ s-Group BY
                      Auto)
          THEN RepeatFor 2 ((D 1 THENA Auto))
          THEN All (Folds ``sg-op sg-inv``)
          THEN DoSubsume
          THEN Try (Trivial)
          THEN Unfold `all` 0
          THEN Auto)
         ORELSE (MemTypeCD THEN Reduce 0 THEN Auto)
         ORELSE Auto)) }

---

Latex:

---

Latex:
\mforall{}[sg:s-Group].  \mforall{}[P:Point  {}\mrightarrow{}  \mBbbP{}].    mk-s-subgroup(sg;x.P[x])  \mmember{}  s-Group  supposing  sg-subgroup(sg;x.P[x])


By

---

Latex:
((Auto  THEN  D  -1  THEN  ExRepD)
  THEN  Unfold  `mk-s-subgroup`  0
  THEN  MemCD
  THEN  (All    (RWO  "set-ss-point  set-ss-eq  set-ss-sep")  THENA  Auto)
  THEN  ((Reduce  0
                THEN  (Assert  sg  \mmember{}  s-Group  BY
                                        Auto)
                THEN  RepeatFor  2  ((D  1  THENA  Auto))
                THEN  All  (Folds  ``sg-op  sg-inv``)
                THEN  DoSubsume
                THEN  Try  (Trivial)
                THEN  Unfold  `all`  0
                THEN  Auto)
              ORELSE  (MemTypeCD  THEN  Reduce  0  THEN  Auto)
              ORELSE  Auto))

---

Home Index