---

Step * of Lemma regext_wf

∀[a:coSet{i:l}]. (regext(a) ∈ coSet{i:l})
BY
{ ((Auto THEN coSetD 1 THEN D 1) THEN RepUR ``regext mk-set Wsup`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a:coSet\{i:l\}].  (regext(a)  \mmember{}  coSet\{i:l\})


By

---

Latex:
((Auto  THEN  coSetD  1  THEN  D  1)  THEN  RepUR  ``regext  mk-set  Wsup``  0  THEN  Auto)

---

Home Index