---

Step * of Lemma member-parallel-class

∀[Info,A:Type]. ∀[X,Y:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E].  uiff(↑e ∈b X || Y;↑(e ∈b X ∨be ∈b Y))
BY
{ ((UnivCD THENA Auto) THEN D 0 THEN (UnivCD THENA Auto)) }

1
1. Info : Type
2. A : Type
3. X : EClass(A)
4. Y : EClass(A)
5. es : EO+(Info)
6. e : E
7. ↑e ∈b X || Y
⊢ ↑(e ∈b X ∨be ∈b Y)

2
1. Info : Type
2. A : Type
3. X : EClass(A)
4. Y : EClass(A)
5. es : EO+(Info)
6. e : E
7. ↑(e ∈b X ∨be ∈b Y)
⊢ ↑e ∈b X || Y

---

Latex:

---

Latex:
\mforall{}[Info,A:Type].  \mforall{}[X,Y:EClass(A)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].    uiff(\muparrow{}e  \mmember{}\msubb{}  X  ||  Y;\muparrow{}(e  \mmember{}\msubb{}  X  \mvee{}\msubb{}e  \mmember{}\msubb{}  Y))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  D  0  THEN  (UnivCD  THENA  Auto))

---

Home Index