Let alpha, beta, p and q be given.

Assume H1.

We will prove PNoLt_ (alpha ∩ beta) p q ∨ alpha ∈ beta ∧ PNoEq_ alpha p q ∧ q alpha ∨ beta ∈ alpha ∧ PNoEq_ beta p q ∧ ¬ p beta.

Apply or3I1 to the current goal.

An exact proof term for the current goal is H1.

∎