---

Step * of Lemma seteq-iff-setsubset

∀a,b:coSet{i:l}.  (seteq(a;b) ⇐⇒ (a ⊆ b) ∧ (b ⊆ a))
BY
{ (Intros THEN RWO  "setsubset-iff co-seteq-iff" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a,b:coSet\{i:l\}.    (seteq(a;b)  \mLeftarrow{}{}\mRightarrow{}  (a  \msubseteq{}  b)  \mwedge{}  (b  \msubseteq{}  a))


By

---

Latex:
(Intros  THEN  RWO    "setsubset-iff  co-seteq-iff"  0  THEN  Auto)

---

Home Index