Let X, Tx, Y and Ty be given.
Assume HX: Hausdorff_space X Tx.
Assume HY: Hausdorff_space Y Ty.
We will prove Hausdorff_space (setprod X Y) (product_topology X Tx Y Ty).
Apply (Hausdorff_stability X Tx Y Ty) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HX.
An exact proof term for the current goal is HY.
∎