---

Step * of Lemma member-class-output

∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[es:EO+(Info)]. ∀[bg:bag(E)]. ∀[v:T].
  uiff(v ↓∈ class-output(X;es;bg);↓∃e:E. (e ↓∈ bg ∧ v ↓∈ class-le-before(X;es;e)))
BY
{ (((UnivCD THENM Unfold `class-output` 0) THENA Auto)
   THEN Auto
   THEN (BagMemberD (-1) ORELSE BagMemberD 0)
   THEN Trivial) }

---

Latex:


\mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[es:EO+(Info)].  \mforall{}[bg:bag(E)].  \mforall{}[v:T].
    uiff(v  \mdownarrow{}\mmember{}  class-output(X;es;bg);\mdownarrow{}\mexists{}e:E.  (e  \mdownarrow{}\mmember{}  bg  \mwedge{}  v  \mdownarrow{}\mmember{}  class-le-before(X;es;e)))


By

(((UnivCD  THENM  Unfold  `class-output`  0)  THENA  Auto)
  THEN  Auto
  THEN  (BagMemberD  (-1)  ORELSE  BagMemberD  0)
  THEN  Trivial)

---

Home Index