An exact proof term for the current goal is (andER (topology_on X T) (C ⊆ X ∧ ∃U ∈ T, C = X ∖ U) H).