Let X and Tx be given.
Assume Hcomp: compact_space X Tx.
Let N be given.
Assume HN: net_pack_in_space X N.
We will prove ∃sub x : set, subnet_of (net_pack_fun N) sub ∧ net_converges X Tx sub x.
We prove the intermediate claim Hnet: net_in_space X (net_pack_fun N).
An exact proof term for the current goal is (net_pack_in_space_implies_net_in_space X N HN).
An exact proof term for the current goal is (compact_space_implies_every_net_has_convergent_subnet X Tx Hcomp (net_pack_fun N) Hnet).
∎