Let X and Tx be given.

Assume Hlc: locally_compact X Tx.

Assume HH: Hausdorff_space X Tx.

We will prove ∃Y Ty : set, one_point_compactification X Tx Y Ty.

An exact proof term for the current goal is (one_point_compactification_exists X Tx Hlc HH).

∎