Let X and Tx be given.
Assume Hperf: perfectly_normal_space X Tx.
Set RHS to be the term one_point_sets_closed X Tx ∧ (∀A B : set, separated_subsets X Tx A B → ∃U V : set, open_in X Tx U ∧ open_in X Tx V ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty).
Apply (iffER (completely_normal_space X Tx) RHS (ex32_6_completely_normal_characterization X Tx)) to the current goal.
We will prove RHS.
We prove the intermediate claim Hnorm: normal_space X Tx.
An exact proof term for the current goal is (andEL (normal_space X Tx) (∀A : set, closed_in X Tx A → Gdelta_in X Tx A) Hperf).
We prove the intermediate claim Hone: one_point_sets_closed X Tx.
An exact proof term for the current goal is (andEL (one_point_sets_closed X Tx) (∀A B : set, closed_in X Tx A → closed_in X Tx B → A ∩ B = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty) Hnorm).
Apply andI to the current goal.
An exact proof term for the current goal is Hone.
Let A and B be given.
Assume Hsep: separated_subsets X Tx A B.
We will prove ∃U V : set, open_in X Tx U ∧ open_in X Tx V ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.
The rest of this subproof is missing.
∎