---

Step * 1 of Lemma es-E-filter-image


1. Info : Type
2. A : Type
3. f : A ⟶ bag(Top)
4. es : EO+(Info)
5. X : EClass(A)
⊢ E(f[X]) ⊆r E(X)
BY
{ (D 0⋅ THENA Auto) }

1
.....subterm..... T:t
1:n
1. Info : Type
2. A : Type
3. f : A ⟶ bag(Top)
4. es : EO+(Info)
5. X : EClass(A)
6. x : E(f[X])@i
⊢ x ∈ E(X)

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  f  :  A  {}\mrightarrow{}  bag(Top)
4.  es  :  EO+(Info)
5.  X  :  EClass(A)
\mvdash{}  E(f[X])  \msubseteq{}r  E(X)


By

---

Latex:
(D  0\mcdot{}  THENA  Auto)

---

Home Index