---

Step * of Lemma setmem-loopset

∀z:coSet{i:l}. ((z ∈ loopset()) ⇐⇒ seteq(z;loopset()))
BY
{ Auto }

1
1. z : coSet{i:l}
2. (z ∈ loopset())
⊢ seteq(z;loopset())

2
1. z : coSet{i:l}
2. seteq(z;loopset())
⊢ (z ∈ loopset())

---

Latex:

---

Latex:
\mforall{}z:coSet\{i:l\}.  ((z  \mmember{}  loopset())  \mLeftarrow{}{}\mRightarrow{}  seteq(z;loopset()))


By

---

Latex:
Auto

---

Home Index