---

Step * of Lemma fst-orderedpairset

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

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  Unfold  `orderedpair-fst`  0)  THEN  RWO  "orderedpair-first"  0  THEN  Auto)

---

Home Index