---

Step * 1 of Lemma orderedpair-first

.....assertion..... 
1. a : coSet{i:l}
2. b : coSet{i:l}
⊢ ∃x:coSet{i:l}. (x ∈ (a,b))
BY
{ ((D 0 With ⌜{a}⌝  THEN Auto) THEN Unfold `orderedpairset` 0 THEN RWO "setmem-pairset" 0 THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  a  :  coSet\{i:l\}
2.  b  :  coSet\{i:l\}
\mvdash{}  \mexists{}x:coSet\{i:l\}.  (x  \mmember{}  (a,b))


By

---

Latex:
((D  0  With  \mkleeneopen{}\{a\}\mkleeneclose{}    THEN  Auto)  THEN  Unfold  `orderedpairset`  0  THEN  RWO  "setmem-pairset"  0  THEN  Auto)

---

Home Index