Let Fam be given.

Assume Hcover: open_cover_of X Tx Fam.

We will prove has_finite_subcover X Tx Fam.

Apply (xm (has_finite_subcover X Tx Fam)) to the current goal.

Assume Hfin: has_finite_subcover X Tx Fam.

An exact proof term for the current goal is Hfin.

Assume Hnofin: ¬ (has_finite_subcover X Tx Fam).

Apply FalseE to the current goal.

We prove the intermediate claim Hexnet: ∃N : set, net_pack_in_space X N ∧ (∀S x : set, subnet_pack_of_in X N S → ¬ (net_pack_converges X Tx S x)).

An exact proof term for the current goal is (open_cover_no_finite_subcover_implies_net_pack_counterexample X Tx Fam HTx Hcover Hnofin).

Apply Hexnet to the current goal.

Let N be given.

Assume Hdata: net_pack_in_space X N ∧ (∀S x : set, subnet_pack_of_in X N S → ¬ (net_pack_converges X Tx S x)).

We prove the intermediate claim HN: net_pack_in_space X N.

An exact proof term for the current goal is (andEL (net_pack_in_space X N) (∀S x : set, subnet_pack_of_in X N S → ¬ (net_pack_converges X Tx S x)) Hdata).

We prove the intermediate claim Hno: ∀S x : set, subnet_pack_of_in X N S → ¬ (net_pack_converges X Tx S x).

An exact proof term for the current goal is (andER (net_pack_in_space X N) (∀S x : set, subnet_pack_of_in X N S → ¬ (net_pack_converges X Tx S x)) Hdata).

We prove the intermediate claim Hexsub: ∃S x : set, subnet_pack_of_in X N S ∧ net_pack_converges X Tx S x.

An exact proof term for the current goal is (Hnets N HN).

Apply Hexsub to the current goal.

Let S be given.

Apply Hexx to the current goal.

Let x be given.

We prove the intermediate claim Hsub: subnet_pack_of_in X N S.

An exact proof term for the current goal is (andEL (subnet_pack_of_in X N S) (net_pack_converges X Tx S x) Hsubconv).

We prove the intermediate claim Hconv: net_pack_converges X Tx S x.

An exact proof term for the current goal is (andER (subnet_pack_of_in X N S) (net_pack_converges X Tx S x) Hsubconv).

An exact proof term for the current goal is ((Hno S x Hsub) Hconv).