---

Step * of Lemma member-eclass-iff-non-empty

∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[es:EO+(Info)]. ∀[e:E].  (↑e ∈b X ⇐⇒ ¬((X es e) = {} ∈ bag(T)))
BY
{ ((UnivCD THENA Auto)
   THEN (RWO "member-eclass-iff-size" 0 THENA Auto)
   THEN (GenConclTerm ⌈X es e⌉⋅ THENA Auto)
   THEN All Thin) }

1
1. T : Type
2. v : bag(T)@i
⊢ 0 < #(v) ⇐⇒ ¬(v = {} ∈ bag(T))

---

Latex:


\mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].    (\muparrow{}e  \mmember{}\msubb{}  X  \mLeftarrow{}{}\mRightarrow{}  \mneg{}((X  es  e)  =  \{\}))


By

((UnivCD  THENA  Auto)
  THEN  (RWO  "member-eclass-iff-size"  0  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}X  es  e\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin)

---

Home Index