---

Step * of Lemma is-interface-or

∀[Info:Type]. ∀es:EO+(Info). ∀X,Y:EClass(Top). ∀e:E.  (↑e ∈b (X | Y) ⇐⇒ (↑e ∈b X) ∨ (↑e ∈b Y))
BY
{ (RepUR ``eclass es-interface-or eclass-compose2
           eclass-val in-eclass oob-apply`` 0⋅
   THEN (UnivCD THENA Auto)
   THEN GenConclAtAddr [2;1;1;1;1]
   THEN GenConclAtAddr [2;2;1;1;1]
   THEN RepeatFor 2 (AutoSplit)) }

---

Latex:

---

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


By

---

Latex:
(RepUR  ``eclass  es-interface-or  eclass-compose2
                  eclass-val  in-eclass  oob-apply``  0\mcdot{}
  THEN  (UnivCD  THENA  Auto)
  THEN  GenConclAtAddr  [2;1;1;1;1]
  THEN  GenConclAtAddr  [2;2;1;1;1]
  THEN  RepeatFor  2  (AutoSplit))

---

Home Index