Let R and alpha be given.

Assume Ha.

Let p and q be given.

Assume Hpq: PNoEq_ alpha p q.

Assume H1: PNo_strict_lowerbd R alpha p.

We will prove PNo_strict_lowerbd R alpha q.

Let beta be given.

Assume Hb: ordinal beta.

Let r be given.

Assume H2: R beta r.

We will prove PNoLt alpha q beta r.

Apply PNoEqLt_tra alpha beta Ha Hb 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.

∎