---

Step * 2 1 1 of Lemma equipollent-rationals


1. a1 : ℚ
2. a2 : ℚ
3. qrep(a1) = qrep(a2) ∈ {p:ℤ × ℕ+| ↑is-qrep(p)} 
4. qrep(a1) = a1 ∈ ℚ
5. qrep(a2) = a2 ∈ ℚ
⊢ a1 = a2 ∈ ℚ
BY
{ TACTIC:(HypSubst' (-3) (-2) THEN Auto) }

---

Latex:

---

Latex:

1.  a1  :  \mBbbQ{}
2.  a2  :  \mBbbQ{}
3.  qrep(a1)  =  qrep(a2)
4.  qrep(a1)  =  a1
5.  qrep(a2)  =  a2
\mvdash{}  a1  =  a2


By

---

Latex:
TACTIC:(HypSubst'  (-3)  (-2)  THEN  Auto)

---

Home Index