---

Step * of Lemma cosetTC_functionality_subset

∀a,b:coSet{i:l}.  ((a ⊆ b) ⇒ (cosetTC(a) ⊆ cosetTC(b)))
BY
{ (Auto THEN All (RWO "setsubset-iff") THEN Auto) }

1
1. a : coSet{i:l}
2. b : coSet{i:l}
3. ∀x:coSet{i:l}. ((x ∈ a) ⇒ (x ∈ b))
4. x : coSet{i:l}
5. (x ∈ cosetTC(a))
⊢ (x ∈ cosetTC(b))

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  All  (RWO  "setsubset-iff")  THEN  Auto)

---

Home Index