Let alpha and beta be given.
Assume Ha Hb.
Let p, q and r be given.
Assume Hpq Hqr.
Apply PNoLtE alpha beta p q Hpq to the current goal.
Assume Hpq1: PNoLt_ (alpha ∩ beta) p q.
Apply Hpq1 to the current goal.
Let delta be given.
Assume Hpq2.
Apply Hpq2 to the current goal.
Assume Hd: delta ∈ alpha ∩ beta.
Apply binintersectE alpha beta delta Hd to the current goal.
Assume Hd1 Hd2.
Assume Hpq3.
Apply Hpq3 to the current goal.
Assume Hpq3.
Apply Hpq3 to the current goal.
Assume Hpq3: PNoEq_ delta p q.
Assume Hpq4: ¬ p delta.
Assume Hpq5: q 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.
An exact proof term for the current goal is Hpq3.
We will prove PNoEq_ delta q r.
Apply PNoEq_antimon_ q r beta Hb delta Hd2 to the current goal.
We will prove PNoEq_ beta q r.
An exact proof term for the current goal is Hqr.
We will prove ¬ p delta.
An exact proof term for the current goal is Hpq4.
We will prove r delta.
An exact proof term for the current goal is iffEL (q delta) (r delta) (Hqr delta Hd2) Hpq5.
Assume Hpq1: alpha ∈ beta.
Assume Hpq2: PNoEq_ alpha p q.
Assume Hpq3: q 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 Hpq1.
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 Hpq2.
We will prove PNoEq_ alpha q r.
Apply PNoEq_antimon_ q r beta Hb alpha Hpq1 to the current goal.
An exact proof term for the current goal is Hqr.
We will prove r alpha.
An exact proof term for the current goal is iffEL (q alpha) (r alpha) (Hqr alpha Hpq1) Hpq3.
Assume Hpq1: beta ∈ alpha.
Assume Hpq2: PNoEq_ beta p q.
Assume Hpq3: ¬ p 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 Hpq1.
We will prove PNoEq_ beta p r.
Apply PNoEq_tra_ beta p q r to the current goal.
An exact proof term for the current goal is Hpq2.
An exact proof term for the current goal is Hqr.
We will prove ¬ p beta.
An exact proof term for the current goal is Hpq3.
∎