See my other comment. You can define R(ℚ) as Dedekind cuts, see that there is a monomorphism I from ℚ to R(ℚ), and then set ℝ = (R(ℚ) \ I(ℚ)) ∪ ℚ. Then you have

See my other comment. You can define R(ℚ) as Dedekind cuts, see that there is a monomorphism I from ℚ to R(ℚ), and then set ℝ = (R(ℚ) \ I(ℚ)) ∪ ℚ. Then you have ℚ ⊂ ℝ and ℝ ≅ R(ℚ). No problem. Except of course if you work in a theorem prover that doesn't support a construction like that.