Let alpha and beta be given.
Assume Ha Hb.
Let p, q and r be given.
Assume Hpq Hqr.
Apply PNoLtE alpha beta q r Hqr to the current goal.
Assume Hqr1: PNoLt_ (alpha ∩ beta) q r.
Apply Hqr1 to the current goal.
Let delta be given.
Assume Hqr2.
Apply Hqr2 to the current goal.
Assume Hd: delta ∈ alpha ∩ beta.
Apply binintersectE alpha beta delta Hd to the current goal.
Assume Hd1 Hd2.
Assume Hqr3.
Apply Hqr3 to the current goal.
Assume Hqr3.
Apply Hqr3 to the current goal.
Assume Hqr3: PNoEq_ delta q r.
Assume Hqr4: ¬ q delta.
Assume Hqr5: r delta.
We will prove PNoLt alpha p beta r.
Apply PNoLtI1 to the current goal.
We will prove ∃delta ∈ alpha ∩ beta, PNoEq_ delta p r ∧ ¬ p delta ∧ r delta.
We use delta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hd.
Apply and3I to the current goal.
We will prove PNoEq_ delta p r.
Apply PNoEq_tra_ delta p q r to the current goal.
We will prove PNoEq_ delta p q.
Apply PNoEq_antimon_ p q alpha Ha delta Hd1 to the current goal.
We will prove PNoEq_ alpha p q.
An exact proof term for the current goal is Hpq.
We will prove PNoEq_ delta q r.
An exact proof term for the current goal is Hqr3.
We will prove ¬ p delta.
Assume H1: p delta.
Apply Hqr4 to the current goal.
We will prove q delta.
An exact proof term for the current goal is iffEL (p delta) (q delta) (Hpq delta Hd1) H1.
We will prove r delta.
An exact proof term for the current goal is Hqr5.
Assume Hqr1: alpha ∈ beta.
Assume Hqr2: PNoEq_ alpha q r.
Assume Hqr3: r alpha.
We will prove PNoLt alpha p beta r.
Apply PNoLtI2 to the current goal.
We will prove alpha ∈ beta.
An exact proof term for the current goal is Hqr1.
We will prove PNoEq_ alpha p r.
Apply PNoEq_tra_ alpha p q r to the current goal.
An exact proof term for the current goal is Hpq.
An exact proof term for the current goal is Hqr2.
We will prove r alpha.
An exact proof term for the current goal is Hqr3.
Assume Hqr1: beta ∈ alpha.
Assume Hqr2: PNoEq_ beta q r.
Assume Hqr3: ¬ q beta.
We will prove PNoLt alpha p beta r.
Apply PNoLtI3 to the current goal.
We will prove beta ∈ alpha.
An exact proof term for the current goal is Hqr1.
We will prove PNoEq_ beta p r.
Apply PNoEq_tra_ beta p q r to the current goal.
Apply PNoEq_antimon_ p q alpha Ha beta Hqr1 to the current goal.
An exact proof term for the current goal is Hpq.
An exact proof term for the current goal is Hqr2.
We will prove ¬ p beta.
Assume H1: p beta.
Apply Hqr3 to the current goal.
An exact proof term for the current goal is iffEL (p beta) (q beta) (Hpq beta Hqr1) H1.
∎