Let y be given.

Assume H1: ordinal (y ').

We prove the intermediate claim L1: {1} ∈ y '.

We will prove {1} ∈ y ∪ {{1}}.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is SingI {1}.

Apply not_ordinal_Sing1 to the current goal.

An exact proof term for the current goal is ordinal_Hered (y ') H1 {1} L1.

∎