---

Step * of Lemma fset-ac-le_weakening_f-subset

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a,b:fset(fset(T))].  fset-ac-le(eq;a;b) supposing a ⊆ b
BY
{ Auto }

1
1. T : Type
2. eq : EqDecider(T)
3. a : fset(fset(T))
4. b : fset(fset(T))
5. a ⊆ b
⊢ fset-ac-le(eq;a;b)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[a,b:fset(fset(T))].    fset-ac-le(eq;a;b)  supposing  a  \msubseteq{}  b


By

---

Latex:
Auto

---

Home Index