---

Step * of Lemma es-interface-or-hasleft

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A,B:EClass(Top)]. ∀[e:E].  oob-hasleft((A | B)(e)) ~ e ∈b A supposing ↑e ∈b (A | B)
BY
{ ((UnivCD THENA Auto)
   THEN MoveToConcl (-1)
   THEN RepUR ``eclass-val es-interface-or in-eclass eclass-compose2 oob-apply`` 0
   THEN RepeatFor 2 (AutoSplit)
   THEN RepUR ``oob-hasleft`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A,B:EClass(Top)].  \mforall{}[e:E].
    oob-hasleft((A  |  B)(e))  \msim{}  e  \mmember{}\msubb{}  A  supposing  \muparrow{}e  \mmember{}\msubb{}  (A  |  B)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  RepUR  ``eclass-val  es-interface-or  in-eclass  eclass-compose2  oob-apply``  0
  THEN  RepeatFor  2  (AutoSplit)
  THEN  RepUR  ``oob-hasleft``  0
  THEN  Auto)

---

Home Index