Let A and B be given.

Assume Hnot: ¬ (B ⊆ A).

Set P to be the term λx : set ⇒ x ∈ B → x ∈ A.

We prove the intermediate claim HnotAll: ¬ (∀x : set, P x).

Assume Hall: ∀x : set, P x.

Apply Hnot to the current goal.

Let x be given.

Assume HxB: x ∈ B.

An exact proof term for the current goal is (Hall x HxB).

Apply (not_all_ex_demorgan_i P HnotAll) to the current goal.

Let x be given.

Assume Hnimp: ¬ P x.

We prove the intermediate claim Hpair: x ∈ B ∧ ¬ (x ∈ A).

An exact proof term for the current goal is (not_imp (x ∈ B) (x ∈ A) Hnimp).

We use x to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (andEL (x ∈ B) (¬ (x ∈ A)) Hpair).

An exact proof term for the current goal is (andER (x ∈ B) (¬ (x ∈ A)) Hpair).

∎