---

Step * of Lemma itersetfun_functionality

∀G:Set{i:l} ⟶ Set{i:l}
  ((∀a,b:Set{i:l}.  ((a ⊆ b) ⇒ (G[a] ⊆ G[b])))
  ⇒ (∀b,a:Set{i:l}.  (seteq(a;b) ⇒ seteq(itersetfun(x.G[x];a);itersetfun(x.G[x];b)))))
BY
{ (Auto THEN (RWO "seteq-iff-setsubset" (-1) THENA Auto) THEN RWO "seteq-iff-setsubset" 0 THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}G:Set\{i:l\}  {}\mrightarrow{}  Set\{i:l\}
    ((\mforall{}a,b:Set\{i:l\}.    ((a  \msubseteq{}  b)  {}\mRightarrow{}  (G[a]  \msubseteq{}  G[b])))
    {}\mRightarrow{}  (\mforall{}b,a:Set\{i:l\}.    (seteq(a;b)  {}\mRightarrow{}  seteq(itersetfun(x.G[x];a);itersetfun(x.G[x];b)))))


By

---

Latex:
(Auto
  THEN  (RWO  "seteq-iff-setsubset"  (-1)  THENA  Auto)
  THEN  RWO  "seteq-iff-setsubset"  0
  THEN  EAuto  1)

---

Home Index