---

Step * of Lemma setTC-contains

∀a:Set{i:l}. (a ⊆ setTC(a))
BY
{ (RWO "setsubset-iff" 0 THEN Auto THEN Unfold `setTC` 0 THEN RW SetMemC 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a:Set\{i:l\}.  (a  \msubseteq{}  setTC(a))


By

---

Latex:
(RWO  "setsubset-iff"  0  THEN  Auto  THEN  Unfold  `setTC`  0  THEN  RW  SetMemC  0  THEN  Auto)

---

Home Index