Set B to be the term rational_open_intervals_basis.
We prove the intermediate claim HBpkg: basis_on R B ∧ generated_topology R B = R_standard_topology.
An exact proof term for the current goal is ex13_8a_rational_intervals_basis_standard.
We prove the intermediate claim HBbasis: basis_on R B.
An exact proof term for the current goal is (andEL (basis_on R B) (generated_topology R B = R_standard_topology) HBpkg).
We prove the intermediate claim HBeq: generated_topology R B = R_standard_topology.
An exact proof term for the current goal is (andER (basis_on R B) (generated_topology R B = R_standard_topology) HBpkg).
Apply andI to the current goal.
rewrite the current goal using rational_rectangle_basis_eq_product_basis_from (from left to right).
An exact proof term for the current goal is (product_basis_from_is_basis_on R R B B R_standard_topology R_standard_topology HBbasis HBeq HBbasis HBeq).
rewrite the current goal using rational_rectangle_basis_eq_product_basis_from (from left to right).
rewrite the current goal using R2_standard_equals_product (from left to right).
An exact proof term for the current goal is (product_basis_generates_product_topology R R B B R_standard_topology R_standard_topology HBbasis HBeq HBbasis HBeq).
∎