Let X and Tx be given.

Assume Hreg: regular_space X Tx.

Assume Hbasis: locally_finite_basis X Tx.

We will prove metrizable X Tx.

We prove the intermediate claim Hsigma: sigma_locally_finite_basis X Tx.

An exact proof term for the current goal is (locally_finite_basis_imp_sigma_locally_finite_basis X Tx Hbasis).

An exact proof term for the current goal is (Nagata_Smirnov_metrization X Tx Hreg Hsigma).

∎