Let X, Tx, Y, Ty and f be given.

Assume HTx: topology_on X Tx.

Assume HTy: topology_on Y Ty.

Assume Hf: function_on f X Y.

Assume Hcont: ∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx.

Let x be given.

Assume Hx: x ∈ X.

Let V be given.

Assume HV: V ∈ Ty.

Assume Hfx: apply_fun f x ∈ V.

We use (preimage_of X f V) to witness the existential quantifier.

Apply and3I to the current goal.

An exact proof term for the current goal is (Hcont V HV).

We will prove x ∈ preimage_of X f V.

We will prove x ∈ {x ∈ X|apply_fun f x ∈ V}.

An exact proof term for the current goal is (SepI X (λx ⇒ apply_fun f x ∈ V) x Hx Hfx).

Let u be given.

Assume Hu: u ∈ preimage_of X f V.

We will prove apply_fun f u ∈ V.

Apply (SepE X (λx ⇒ apply_fun f x ∈ V) u Hu) to the current goal.

Assume _.

Assume H.

An exact proof term for the current goal is H.

∎