---

Step * of Lemma es-is-interface-union

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

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RepUR  ``eclass  in-eclass  es-interface-union  eclass-compose2``  0\mcdot{}  THEN  Repeat  (AutoSplit))\mcdot{}
  )

---

Home Index