---

Step * 1 of Lemma poset-cat-arrow-unique

.....truecase..... 
1. I : Cname List
2. x : name-morph(I;[])
3. y : name-morph(I;[])
4. a : x@0:nameset(I) ⟶ (↑x x@0 ≤z y x@0)
5. b : x@0:nameset(I) ⟶ (↑x x@0 ≤z y x@0)
6. x@0 : nameset(I)
7. v : True@i
8. (a x@0) = v ∈ (↑x x@0 ≤z y x@0)@i
9. v1 : True@i
10. (b x@0) = v1 ∈ (↑x x@0 ≤z y x@0)@i
11. (x x@0) ≤ (y x@0)
12. (x x@0) ≤ (y x@0)
⊢ v = v1 ∈ (↑x x@0 ≤z y x@0)
BY
{ (DVar `v' THEN DVar `v1' THEN Auto) }

---

Latex:

---

Latex:
.....truecase..... 
1.  I  :  Cname  List
2.  x  :  name-morph(I;[])
3.  y  :  name-morph(I;[])
4.  a  :  x@0:nameset(I)  {}\mrightarrow{}  (\muparrow{}x  x@0  \mleq{}z  y  x@0)
5.  b  :  x@0:nameset(I)  {}\mrightarrow{}  (\muparrow{}x  x@0  \mleq{}z  y  x@0)
6.  x@0  :  nameset(I)
7.  v  :  True@i
8.  (a  x@0)  =  v@i
9.  v1  :  True@i
10.  (b  x@0)  =  v1@i
11.  (x  x@0)  \mleq{}  (y  x@0)
12.  (x  x@0)  \mleq{}  (y  x@0)
\mvdash{}  v  =  v1


By

---

Latex:
(DVar  `v'  THEN  DVar  `v1'  THEN  Auto)

---

Home Index