Let L and alpha be given.

Assume Ha.

Let p and q be given.

Assume Hpq: PNoEq_ alpha p q.

Assume H1: PNo_strict_upperbd L alpha p.

We will prove PNo_strict_upperbd L alpha q.

Let beta be given.

Assume Hb: ordinal beta.

Let r be given.

Assume H2: L beta r.

We will prove PNoLt beta r alpha q.

Apply PNoLtEq_tra beta alpha Hb Ha r p q to the current goal.

We will prove PNoLt beta r alpha p.

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

We will prove PNoEq_ alpha p q.

An exact proof term for the current goal is Hpq.

∎