Step
*
of Lemma
setmem-mk-set-sq
∀[T,f,x:Top]. ((x ∈ f"(T)) ~ ∃b:T. seteq(x;f b))
BY
{ (Auto THEN RepUR ``setmem coWmem coW-dom coW-item mk-set Wsup`` 0 THEN Fold `seteq` 0 THEN Auto) }
Latex:
Latex:
\mforall{}[T,f,x:Top]. ((x \mmember{} f"(T)) \msim{} \mexists{}b:T. seteq(x;f b))
By
Latex:
(Auto THEN RepUR ``setmem coWmem coW-dom coW-item mk-set Wsup`` 0 THEN Fold `seteq` 0 THEN Auto)
Home
Index