Let X, Tx and U be given.

Assume HTx: topology_on X Tx.

Assume Hcover: open_cover X Tx U.

We will prove U ⊆ 𝒫 X.

Let u be given.

Assume HuU: u ∈ U.

We will prove u ∈ 𝒫 X.

We prove the intermediate claim HuTx: u ∈ Tx.

An exact proof term for the current goal is (open_cover_members_open X Tx U u Hcover HuU).

An exact proof term for the current goal is (topology_subset_axiom X Tx HTx u HuTx).

∎