Let X and Tx be given.

Apply iffI to the current goal.

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

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

∎