---

{ [Info:Type]
    es:EO+(Info)
      [A:Type]
        X,Y:EClass(A). e:E.  (e  [X?Y]  (e  X)  (e  Y)) }

{ Proof }

---

Definitions occuring in Statement :  cond-class: [X?Y],  in-eclass: e  X,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-E: E,  assert: b,  uall: [x:A]. B[x],  all: x:A. B[x],  iff: P  Q,  or: P  Q,  universe: Type
Definitions :  isect: x:A. B[x],  uall: [x:A]. B[x],  CollapseTHEN: Error :CollapseTHEN,  tactic: Error :tactic
Lemmas :  es-interface-conditional-domain-iff

---

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


Date html generated: 2011_08_16-AM-11_43_01
Last ObjectModification: 2011_06_20-AM-00_33_42

Home Index