Assume Heq: rational_numbers = setprod 2 ω.

We will prove False.

Apply setprod_2_omega_neq_rational_numbers to the current goal.

rewrite the current goal using Heq (from right to left).

Use reflexivity.

∎