Let α, β, p and q be given.

Assume H1.

We will prove PNoLt_ (α ∩ β) p q ∨ α ∈ β ∧ PNoEq_ α p q ∧ q α ∨ β ∈ α ∧ PNoEq_ β p q ∧ ¬ p β.

Apply or3I1 to the current goal.

An exact proof term for the current goal is H1.

∎