---

Step * of Lemma assert-fset-null

∀[T:Type]. ∀[s:fset(T)].  uiff(↑fset-null(s);s = {} ∈ fset(T))
BY
{ Auto }

1
1. T : Type
2. s : fset(T)
3. ↑fset-null(s)
⊢ s = {} ∈ fset(T)

2
1. T : Type
2. s : fset(T)
3. s = {} ∈ fset(T)
⊢ ↑fset-null(s)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[s:fset(T)].    uiff(\muparrow{}fset-null(s);s  =  \{\})


By

---

Latex:
Auto

---

Home Index