---

Step * of Lemma is-prior-class-when

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X,Y:EClass(Top)]. ∀[d:Top]. ∀[e:E].  (e ∈b (X'?d) when Y ~ e ∈b Y)
BY
{ (UnivCD THENA Auto) }

1
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. Y : EClass(Top)
5. d : Top
6. e : E
⊢ e ∈b (X'?d) when Y ~ e ∈b Y

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X,Y:EClass(Top)].  \mforall{}[d:Top].  \mforall{}[e:E].    (e  \mmember{}\msubb{}  (X'?d)  when  Y  \msim{}  e  \mmember{}\msubb{}  Y)


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index