Apply ZF_ordsucc_closed with
prim6 0,
0 leaving 2 subgoals.
The subproof is completed by applying UnivOf_ZF_closed with 0.
Apply unknownprop_e747e5ba1c4c5fc029f52d44d14d3be2d06759ee5e8f12e8b1e65810154eb535 with
prim6 0,
0 leaving 3 subgoals.
The subproof is completed by applying UnivOf_TransSet with 0.
The subproof is completed by applying UnivOf_ZF_closed with 0.
The subproof is completed by applying UnivOf_In with 0.
Apply unknownprop_b6fb54fab4516b035f62dacd09064964d22d891fcede06066aa8011a5caac6b6 with
λ x0 . x0 ∈ prim6 0.
The subproof is completed by applying L0.