Let X, Tx and m be given.

Assume Hloc: locally_m_euclidean X Tx m.

Assume Hnorm: normal_space X Tx.

We will prove Hausdorff_space X Tx.

We prove the intermediate claim HT1: T1_space X Tx.

An exact proof term for the current goal is (locally_m_euclidean_implies_T1 X Tx m Hloc).

An exact proof term for the current goal is (normal_T1_implies_Hausdorff X Tx Hnorm HT1).

∎