Let R and α be given.
Assume Ha.
Let p and q be given.
Assume Hpq: PNoEq_ α p q.
Assume H1: PNo_rel_strict_lowerbd R α p.
We will prove PNo_rel_strict_lowerbd R α q.
Let β be given.
Assume Hb: β ∈ α.
Let r be given.
Assume H2: PNo_upc R β r.
We prove the intermediate claim Lb: ordinal β.
An exact proof term for the current goal is ordinal_Hered α Ha β Hb.
We will prove PNoLt α q β r.
Apply PNoEqLt_tra α β Ha Lb q p r to the current goal.
We will prove PNoEq_ α q p.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is Hpq.
We will prove PNoLt α p β r.
An exact proof term for the current goal is H1 β Hb r H2.
∎