Let U and X be given.

Assume H1 H2 H3.

Apply ZF_closed_E U H2 to the current goal.

Assume HU HP HR.

We prove the intermediate claim L1: 𝒫 X ∈ U.

Apply HP to the current goal.

An exact proof term for the current goal is H3.

Apply H1 (𝒫 X) L1 0 to the current goal.

We will prove 0 ∈ 𝒫 X.

Apply Empty_In_Power to the current goal.

∎