Let X, T and C be given.

Assume H: closed_in X T C.

We prove the intermediate claim Hpack: C ⊆ X ∧ ∃U ∈ T, C = X ∖ U.

An exact proof term for the current goal is (closed_in_package X T C H).

An exact proof term for the current goal is (andER (C ⊆ X) (∃U ∈ T, C = X ∖ U) Hpack).

∎