---

Step * of Lemma setmem-set-part

∀s,x:coSet{i:l}.  ((x ∈ set-part(s)) ⇐⇒ (x ∈ s) ∧ isSet(x))
BY
{ (Intros THEN Unfold `set-part` 0 THEN RWO "setmem-sub-coset" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}s,x:coSet\{i:l\}.    ((x  \mmember{}  set-part(s))  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  s)  \mwedge{}  isSet(x))


By

---

Latex:
(Intros  THEN  Unfold  `set-part`  0  THEN  RWO  "setmem-sub-coset"  0  THEN  Auto)

---

Home Index