---

Step * of Lemma cosetTC-contains

∀a:coSet{i:l}. (a ⊆ cosetTC(a))
BY
{ (RWO "setsubset-iff" 0
   THEN Auto
   THEN SetMemDef 0
   THEN D -1
   THEN RepUR ``seteq`` 0
   THEN D 0 With ⌜copath-cons(b;())⌝ 
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a:coSet\{i:l\}.  (a  \msubseteq{}  cosetTC(a))


By

---

Latex:
(RWO  "setsubset-iff"  0
  THEN  Auto
  THEN  SetMemDef  0
  THEN  D  -1
  THEN  RepUR  ``seteq``  0
  THEN  D  0  With  \mkleeneopen{}copath-cons(b;())\mkleeneclose{} 
  THEN  Auto)

---

Home Index