---

Step * of Lemma snd-orderedpairset

∀a,b:coSet{i:l}.  seteq(snd((a,b));b)
BY
{ ((Auto THEN Unfold `orderedpair-snd` 0) THEN RWO "orderedpair-second" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a,b:coSet\{i:l\}.    seteq(snd((a,b));b)


By

---

Latex:
((Auto  THEN  Unfold  `orderedpair-snd`  0)  THEN  RWO  "orderedpair-second"  0  THEN  Auto)

---

Home Index