Let L and α be given.

Assume Ha.

Let p and q be given.

Assume Hpq: PNoEq_ α p q.

Assume H1: PNo_strict_upperbd L α p.

We will prove PNo_strict_upperbd L α q.

Let β be given.

Assume Hb: ordinal β.

Let r be given.

Assume H2: L β r.

We will prove PNoLt β r α q.

Apply PNoLtEq_tra β α Hb Ha r p q to the current goal.

We will prove PNoLt β r α p.

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

We will prove PNoEq_ α p q.

An exact proof term for the current goal is Hpq.

∎