We will prove basis_generates EuclidPlane rectangular_regions R2_standard_topology.

We will prove basis_on EuclidPlane rectangular_regions ∧ generated_topology EuclidPlane rectangular_regions = R2_standard_topology.

Apply andI to the current goal.

An exact proof term for the current goal is rectangular_regions_basis_plane.

An exact proof term for the current goal is generated_topology_rectangular_regions_eq_R2_standard_topology.

∎