Let L and α be given.
Assume Ha.
Let p and q be given.
Assume Hpq: PNoEq_ α p q.
Assume H1: PNo_rel_strict_upperbd L α p.
We will prove PNo_rel_strict_upperbd L α q.
Let β be given.
Assume Hb: β ∈ α.
Let r be given.
Assume H2: PNo_downc L β 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 β r α q.
Apply PNoLtEq_tra β α Lb 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.
∎