Let L and alpha be given.
Assume Ha.
Let p and q be given.
Assume Hpq: PNoEq_ alpha p q.
Assume H1: PNo_rel_strict_upperbd L alpha p.
We will prove PNo_rel_strict_upperbd L alpha q.
Let beta be given.
Assume Hb: beta ∈ alpha.
Let r be given.
Assume H2: PNo_downc L beta r.
We prove the intermediate claim Lb: ordinal beta.
An exact proof term for the current goal is ordinal_Hered alpha Ha beta Hb.
We will prove PNoLt beta r alpha q.
Apply PNoLtEq_tra beta alpha Lb 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.
∎