---

Step * of Lemma is-cond-class

∀[Info:Type]. ∀X,Y:EClass(Top). ∀es:EO+(Info). ∀e:E.  (↑e ∈b [X?Y] ⇐⇒ (↑e ∈b X) ∨ (↑e ∈b Y))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``in-eclass cond-class eclass-compose2`` 0⋅ THEN AutoSplit) }

---

Latex:


\mforall{}[Info:Type].  \mforall{}X,Y:EClass(Top).  \mforall{}es:EO+(Info).  \mforall{}e:E.    (\muparrow{}e  \mmember{}\msubb{}  [X?Y]  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}e  \mmember{}\msubb{}  X)  \mvee{}  (\muparrow{}e  \mmember{}\msubb{}  Y))


By

((UnivCD  THENA  Auto)  THEN  RepUR  ``in-eclass  cond-class  eclass-compose2``  0\mcdot{}  THEN  AutoSplit)

---

Home Index