---

Step * of Lemma setTC_functionality

∀a,b:Set{i:l}.  (seteq(a;b) ⇒ seteq(setTC(a);setTC(b)))
BY
{ (RWO "seteq-iff-setsubset" 0 THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}a,b:Set\{i:l\}.    (seteq(a;b)  {}\mRightarrow{}  seteq(setTC(a);setTC(b)))


By

---

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

---

Home Index