Let X and Tx be given.

Assume H1: closed_in X Tx X.

Assume H2: ∀A : set, closed_in X Tx A → closed_in X Tx (X ∖ A).

We will prove topology_on X Tx.

An exact proof term for the current goal is (andEL (topology_on X Tx) (X ⊆ X ∧ ∃U ∈ Tx, X = X ∖ U) H1).

∎