Let X, Tx, N and x be given.

Assume H: net_pack_converges X Tx N x.

We will prove topology_on X Tx.

Apply H to the current goal.

Let J be given.

Assume Hexle: ∃le net : set, N = net_pack J le net ∧ net_converges_on X Tx net J le x.

Apply Hexle to the current goal.

Let le be given.

Assume Hexnet: ∃net : set, N = net_pack J le net ∧ net_converges_on X Tx net J le x.

Apply Hexnet to the current goal.

Let net be given.

Assume Hpair: N = net_pack J le net ∧ net_converges_on X Tx net J le x.

We prove the intermediate claim Hconv: net_converges_on X Tx net J le x.

An exact proof term for the current goal is (andER (N = net_pack J le net) (net_converges_on X Tx net J le x) Hpair).

Apply Hconv to the current goal.

Assume Hcore Htail.

Apply Hcore to the current goal.

Assume Hcore5 HxX.

Apply Hcore5 to the current goal.

Assume Hcore4 Hdom.

Apply Hcore4 to the current goal.

Assume Hcore3 Hgraph.

Apply Hcore3 to the current goal.

Assume Hcore2 Htot.

Apply Hcore2 to the current goal.

Assume HTx Hdir.

An exact proof term for the current goal is HTx.

∎