---

Step * of Lemma set-item_wf

∀[s:coSet{i:l}]. ∀[x:set-dom(s)].  (set-item(s;x) ∈ coSet{i:l})
BY
{ (Auto THEN coSetD 1⋅ THEN RepUR ``set-dom mk-set Wsup`` -1 THEN RepUR ``set-item mk-set Wsup`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[s:coSet\{i:l\}].  \mforall{}[x:set-dom(s)].    (set-item(s;x)  \mmember{}  coSet\{i:l\})


By

---

Latex:
(Auto
  THEN  coSetD
  1\mcdot{}
  THEN  RepUR  ``set-dom  mk-set  Wsup``  -1
  THEN  RepUR  ``set-item  mk-set  Wsup``  0
  THEN  Auto)

---

Home Index