Let X and Tx be given.

Assume Hcomp: compact_space X Tx.

Let net be given.

Assume Hnet: net_in_space X net.

We will prove ∃sub x : set, subnet_of net sub ∧ net_converges X Tx sub x.

We prove the intermediate claim Hexacc: ∃x0 : set, accumulation_point_of_net X Tx net x0.

An exact proof term for the current goal is (compact_space_net_has_accumulation_point X Tx net Hcomp Hnet).

Apply Hexacc to the current goal.

Let x0 be given.

Assume Hacc: accumulation_point_of_net X Tx net x0.

We prove the intermediate claim Hexsub: ∃sub : set, subnet_of net sub ∧ net_converges X Tx sub x0.

An exact proof term for the current goal is (subnet_converges_to_accumulation X Tx net x0 Hacc).

Apply Hexsub to the current goal.

Let sub be given.

Assume Hsubconv: subnet_of net sub ∧ net_converges X Tx sub x0.

We use sub to witness the existential quantifier.

We use x0 to witness the existential quantifier.

An exact proof term for the current goal is Hsubconv.

∎