Assume Hpq1: PNoLt_ (α ∩ β) p q.

Apply Hpq1 to the current goal.

Let δ be given.

Assume Hpq2.

Apply Hpq2 to the current goal.

Assume Hd: δ ∈ α ∩ β.

Apply binintersectE α β δ 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_ δ p q.

Assume Hpq4: ¬ p δ.

Assume Hpq5: q δ.

We will prove PNoLt α p β r.

Apply PNoLtI1 to the current goal.

We will prove ∃δ ∈ α ∩ β, PNoEq_ δ p r ∧ ¬ p δ ∧ r δ.

We use δ 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_ δ p r.

Apply PNoEq_tra_ δ p q r to the current goal.

We will prove PNoEq_ δ p q.

An exact proof term for the current goal is Hpq3.

We will prove PNoEq_ δ q r.

Apply PNoEq_antimon_ q r β Hb δ Hd2 to the current goal.

We will prove PNoEq_ β q r.

An exact proof term for the current goal is Hqr.

We will prove ¬ p δ.

An exact proof term for the current goal is Hpq4.

We will prove r δ.

An exact proof term for the current goal is iffEL (q δ) (r δ) (Hqr δ Hd2) Hpq5.

Assume Hpq1: α ∈ β.

Assume Hpq2: PNoEq_ α p q.

Assume Hpq3: q α.

We will prove PNoLt α p β r.

Apply PNoLtI2 to the current goal.

We will prove α ∈ β.

An exact proof term for the current goal is Hpq1.

We will prove PNoEq_ α p r.

Apply PNoEq_tra_ α p q r to the current goal.

An exact proof term for the current goal is Hpq2.

We will prove PNoEq_ α q r.

Apply PNoEq_antimon_ q r β Hb α Hpq1 to the current goal.

An exact proof term for the current goal is Hqr.

We will prove r α.

An exact proof term for the current goal is iffEL (q α) (r α) (Hqr α Hpq1) Hpq3.

Assume Hpq1: β ∈ α.

Assume Hpq2: PNoEq_ β p q.

Assume Hpq3: ¬ p β.

We will prove PNoLt α p β r.

Apply PNoLtI3 to the current goal.

We will prove β ∈ α.

An exact proof term for the current goal is Hpq1.

We will prove PNoEq_ β p r.

Apply PNoEq_tra_ β 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 β.

An exact proof term for the current goal is Hpq3.