---

Step * of Lemma fset-ac-le-implies2

∀[T:Type]
  ∀eq:EqDecider(T). ∀ac1,ac2:fset(fset(T)).
    (fset-ac-le(eq;ac1;ac2) ⇒ {∀a:fset(T). (a ∈ ac1 ⇒ (↓∃b:fset(T). (b ∈ ac2 ∧ b ⊆ a)))})
BY
{ (Auto THEN (RWO  "fset-ac-le-iff" (-1) THENA Auto) THEN Unfold `guard` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}ac1,ac2:fset(fset(T)).
        (fset-ac-le(eq;ac1;ac2)  {}\mRightarrow{}  \{\mforall{}a:fset(T).  (a  \mmember{}  ac1  {}\mRightarrow{}  (\mdownarrow{}\mexists{}b:fset(T).  (b  \mmember{}  ac2  \mwedge{}  b  \msubseteq{}  a)))\})


By

---

Latex:
(Auto  THEN  (RWO    "fset-ac-le-iff"  (-1)  THENA  Auto)  THEN  Unfold  `guard`  0  THEN  Auto)

---

Home Index