Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι → ο be given.

Let x3 of type ι → ο be given.

Assume H0: PNoLt x0 x2 x1 x3.

Let x4 of type ο be given.

Assume H1: PNoLt_ (binintersect x0 x1) x2 x3 ⟶ x4.

Assume H2: x0 ∈ x1 ⟶ PNoEq_ x0 x2 x3 ⟶ x3 x0 ⟶ x4.

Assume H3: x1 ∈ x0 ⟶ PNoEq_ x1 x2 x3 ⟶ not (x2 x1) ⟶ x4.

Apply H0 with x4 leaving 2 subgoals.

Assume H4: or (PNoLt_ (binintersect x0 x1) x2 x3) (and (and (x0 ∈ x1) (PNoEq_ x0 x2 x3)) (x3 x0)).

Apply H4 with x4 leaving 2 subgoals.

The subproof is completed by applying H1.

Assume H5: and (and (x0 ∈ x1) (PNoEq_ x0 x2 x3)) (x3 x0).

Apply H5 with x4.

Assume H6: and (x0 ∈ x1) (PNoEq_ x0 x2 x3).

Apply H6 with x3 x0 ⟶ x4.

The subproof is completed by applying H2.

Assume H4: and (and (x1 ∈ x0) (PNoEq_ x1 x2 x3)) (not (x2 x1)).

Apply H4 with x4.

Assume H5: and (x1 ∈ x0) (PNoEq_ x1 x2 x3).

Apply H5 with not (x2 x1) ⟶ x4.

The subproof is completed by applying H3.

■

Proofgold Proof