---

Step * of Lemma seteq_functionality

∀x1,x2,y1,y2:coSet{i:l}.  (seteq(x1;x2) ⇒ seteq(y1;y2) ⇒ (seteq(x1;y1) ⇐⇒ seteq(x2;y2)))
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}x1,x2,y1,y2:coSet\{i:l\}.    (seteq(x1;x2)  {}\mRightarrow{}  seteq(y1;y2)  {}\mRightarrow{}  (seteq(x1;y1)  \mLeftarrow{}{}\mRightarrow{}  seteq(x2;y2)))


By

---

Latex:
Auto

---

Home Index