---

Step * of Lemma Regularcoset_wf

∀[A:coSet{i:l}]. (cRegular(A) ∈ ℙ{i''})
BY
{ ((ProveWfLemma THEN (RWO "transitive-set-iff" 2 THENA Auto) THEN (RWO "setsubset-iff" 2 THENA Auto))
   THEN DoSubsume
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:coSet\{i:l\}].  (cRegular(A)  \mmember{}  \mBbbP{}\{i''\})


By

---

Latex:
((ProveWfLemma  THEN  (RWO  "transitive-set-iff"  2  THENA  Auto)  THEN  (RWO  "setsubset-iff"  2  THENA  Auto))
  THEN  DoSubsume
  THEN  Auto)

---

Home Index