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