---

Step * of Lemma req-rat2real

No Annotations
∀q1,q2:ℚ.  uiff(rat2real(q1) = rat2real(q2);q1 = q2 ∈ ℚ)
BY
{ Auto }

1
1. q1 : ℚ
2. q2 : ℚ
3. rat2real(q1) = rat2real(q2)
⊢ q1 = q2 ∈ ℚ

---

Latex:

---

Latex:
No  Annotations
\mforall{}q1,q2:\mBbbQ{}.    uiff(rat2real(q1)  =  rat2real(q2);q1  =  q2)


By

---

Latex:
Auto

---

Home Index