Let N and X be given.

Assume HX: X ∈ UnivOf N.

Let Q be given.

Assume HQ: Q ⊆ X.

We prove the intermediate claim LZ: ZF_closed (UnivOf N).

An exact proof term for the current goal is UnivOf_ZF_closed N.

We prove the intermediate claim LQ: Q ∈ 𝒫 X.

An exact proof term for the current goal is PowerI X Q HQ.

An exact proof term for the current goal is UnivOf_TransSet N (𝒫 X) (ZF_Power_closed (UnivOf N) LZ X HX) Q LQ.

∎