---

Step * of Lemma empty-fset-contains-none-of

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[cs:fset(fset(T))].  ↑fset-contains-none-of(eq;{};cs) supposing ¬{} ∈ cs
BY
{ ((UnivCD THENA Auto)
   THEN RWO "assert-fset-contains-none-of" 0
   THEN Auto
   THEN RWO  "f-subset-empty" 0
   THEN Auto
   THEN (D 0 THENA Auto)) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[cs:fset(fset(T))].
    \muparrow{}fset-contains-none-of(eq;\{\};cs)  supposing  \mneg{}\{\}  \mmember{}  cs


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RWO  "assert-fset-contains-none-of"  0
  THEN  Auto
  THEN  RWO    "f-subset-empty"  0
  THEN  Auto
  THEN  (D  0  THENA  Auto))

---

Home Index