Assume Hqr1: PNoLt_ (α ∩ β) q r.

Apply Hqr1 to the current goal.

Let δ be given.

Assume Hqr2.

Apply Hqr2 to the current goal.

Assume Hd: δ ∈ α ∩ β.

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

Assume Hqr4: ¬ q δ.

Assume Hqr5: r δ.

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.

Apply PNoEq_antimon_ p q α Ha δ Hd1 to the current goal.

We will prove PNoEq_ α p q.

An exact proof term for the current goal is Hpq.

We will prove PNoEq_ δ q r.

An exact proof term for the current goal is Hqr3.

We will prove ¬ p δ.

Assume H1: p δ.

Apply Hqr4 to the current goal.

We will prove q δ.

An exact proof term for the current goal is iffEL (p δ) (q δ) (Hpq δ Hd1) H1.

We will prove r δ.

An exact proof term for the current goal is Hqr5.

Assume Hqr1: α ∈ β.

Assume Hqr2: PNoEq_ α q r.

Assume Hqr3: r α.

We will prove PNoLt α p β r.

Apply PNoLtI2 to the current goal.

We will prove α ∈ β.

An exact proof term for the current goal is Hqr1.

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 Hpq.

An exact proof term for the current goal is Hqr2.

We will prove r α.

An exact proof term for the current goal is Hqr3.

Assume Hqr1: β ∈ α.

Assume Hqr2: PNoEq_ β q r.

Assume Hqr3: ¬ q β.

We will prove PNoLt α p β r.

Apply PNoLtI3 to the current goal.

We will prove β ∈ α.

An exact proof term for the current goal is Hqr1.

We will prove PNoEq_ β p r.

Apply PNoEq_tra_ β p q r to the current goal.

Apply PNoEq_antimon_ p q α Ha β 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 β.

Assume H1: p β.

Apply Hqr3 to the current goal.

An exact proof term for the current goal is iffEL (p β) (q β) (Hpq β Hqr1) H1.