We will prove countable_set Sorgenfrey_plane_rational_points.

We will prove countable Sorgenfrey_plane_rational_points.

We prove the intermediate claim HQ: countable rational_numbers.

An exact proof term for the current goal is rational_numbers_countable.

An exact proof term for the current goal is (setprod_countable rational_numbers rational_numbers HQ HQ).

∎