Let L and R be given.

Assume HLR.

Let α be given.

Assume Ha HaL HaR.

Apply PNo_bd_pred L R HLR α Ha HaL HaR to the current goal.

Assume H1.

Apply H1 to the current goal.

Assume H1: ordinal (PNo_bd L R).

Assume H2: PNo_strict_imv L R (PNo_bd L R) (PNo_pred L R).

Assume H3: ∀γ ∈ PNo_bd L R, ∀q : set → prop, ¬ PNo_strict_imv L R γ q.

Apply PNo_lenbdd_strict_imv_ex L R HLR α Ha HaL HaR to the current goal.

Let β be given.

Assume H4.

Apply H4 to the current goal.

Assume Hb: β ∈ ordsucc α.

Assume H4.

Apply H4 to the current goal.

Let p be given.

Assume Hp: PNo_strict_imv L R β p.

We prove the intermediate claim Lsa: ordinal (ordsucc α).

An exact proof term for the current goal is ordinal_ordsucc α Ha.

Apply ordinal_In_Or_Subq (PNo_bd L R) (ordsucc α) H1 Lsa to the current goal.

Assume H4: PNo_bd L R ∈ ordsucc α.

An exact proof term for the current goal is H4.

Assume H4: ordsucc α ⊆ PNo_bd L R.

We will prove False.

We prove the intermediate claim Lb: β ∈ PNo_bd L R.

Apply H4 to the current goal.

An exact proof term for the current goal is Hb.

Apply H3 β Lb p to the current goal.

An exact proof term for the current goal is Hp.

∎