---

Step * 1 of Lemma equipollent-quotient

.....aux..... 
1. A : Type
2. E : A ⟶ A ⟶ 𝔹
3. EquivRel(A;x,y.↑(E x y))
4. z : Base
5. z1 : Base
6. z = z1 ∈ (x,y:A//(↑(E x y)))
7. z ∈ A
8. z1 ∈ A
9. ↑(E z z1)
10. x : A
11. ↑(E z x)
⊢ ↑(E z1 x)
BY
{ UseTrans ⌜z⌝⋅ }

---

Latex:

---

Latex:
.....aux..... 
1.  A  :  Type
2.  E  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}
3.  EquivRel(A;x,y.\muparrow{}(E  x  y))
4.  z  :  Base
5.  z1  :  Base
6.  z  =  z1
7.  z  \mmember{}  A
8.  z1  \mmember{}  A
9.  \muparrow{}(E  z  z1)
10.  x  :  A
11.  \muparrow{}(E  z  x)
\mvdash{}  \muparrow{}(E  z1  x)


By

---

Latex:
UseTrans  \mkleeneopen{}z\mkleeneclose{}\mcdot{}

---

Home Index