Let R and alpha be given.

Assume Ha.

Let p and q be given.

Assume Hpq: PNoEq_ alpha p q.

We will prove PNo_rel_strict_lowerbd R alpha q.

Let beta be given.

Assume Hb: beta ∈ alpha.

Let r be given.

Assume H2: PNo_upc R beta r.

We prove the intermediate claim Lb: ordinal beta.

An exact proof term for the current goal is ordinal_Hered alpha Ha beta Hb.

We will prove PNoLt alpha q beta r.

Apply PNoEqLt_tra alpha beta Ha Lb q p r to the current goal.

We will prove PNoEq_ alpha q p.

Apply PNoEq_sym_ to the current goal.

An exact proof term for the current goal is Hpq.

We will prove PNoLt alpha p beta r.

An exact proof term for the current goal is H1 beta Hb r H2.

∎