---

Step * of Lemma Regularset_wf

∀[A:Set{i:l}]. (Regular(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:Set\{i:l\}].  (Regular(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