---

Step * of Lemma is-interface-conditional

∀[Info:Type]. ∀es:EO+(Info). ∀X,Y:EClass(Top). ∀e:E.  (↑e ∈b [X?Y] ⇐⇒ (↑e ∈b X) ∨ (↑e ∈b Y))
BY
{ ((UnivCD THENA Auto) THEN RWO  "is-cond-class" 0 THEN Auto) }

---

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:
((UnivCD  THENA  Auto)  THEN  RWO    "is-cond-class"  0  THEN  Auto)

---

Home Index