We will prove R2_standard_topology = generated_topology EuclidPlane rectangular_regions.
Use symmetry.
An exact proof term for the current goal is generated_topology_rectangular_regions_eq_R2_standard_topology.
∎