---

Step * of Lemma setmem-mkset-sq

∀[T,f,x:Top].  ((x ∈ {f[b] | b ∈ T}) ~ ∃b:T. seteq(x;f[b]))
BY
{ (Auto THEN RepUR ``setmem coWmem coW-dom coW-item mkset Wsup`` 0 THEN Fold `seteq` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,f,x:Top].    ((x  \mmember{}  \{f[b]  |  b  \mmember{}  T\})  \msim{}  \mexists{}b:T.  seteq(x;f[b]))


By

---

Latex:
(Auto  THEN  RepUR  ``setmem  coWmem  coW-dom  coW-item  mkset  Wsup``  0  THEN  Fold  `seteq`  0  THEN  Auto)

---

Home Index