Let X, T and C be given.
Assume HT: topology_on X T.
Assume HCsub: C ⊆ X.
Assume Hex: ∃U ∈ T, C = X ∖ U.
An exact proof term for the current goal is (andI (topology_on X T) (C ⊆ X ∧ ∃U ∈ T, C = X ∖ U) HT (andI (C ⊆ X) (∃U ∈ T, C = X ∖ U) HCsub Hex)).
∎