We prove the intermediate claim L1: ∀X Y ∈ UnivOf (UnivOf Empty), X ⨯ Y ∈ UnivOf (UnivOf Empty).

An exact proof term for the current goal is ZF_setprod_closed (UnivOf (UnivOf Empty)) (UnivOf_TransSet (UnivOf Empty)) (UnivOf_ZF_closed (UnivOf Empty)).

An exact proof term for the current goal is MetaCatSet_product_gen (λX ⇒ X ∈ UnivOf (UnivOf Empty)) L1.

∎