Let X and d be given.

Assume Hd: metric_on X d.

We will prove generated_topology X (famunion X (λx ⇒ {open_ball X d x r|r ∈ R, Rlt 0 r})) = metric_topology X d.

Use reflexivity.

∎