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

Assume Hf: quotient_map X Tx Y f.

Assume HTy: topology_on Y Ty.

Assume Hsub: Ty ⊆ quotient_topology X Tx Y f.

We will prove continuous_map X Tx Y Ty f.

We will prove topology_on X Tx ∧ topology_on Y Ty ∧ function_on f X Y ∧ ∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx.

We prove the intermediate claim Htopfun: topology_on X Tx ∧ function_on f X Y.

An exact proof term for the current goal is (andEL (topology_on X Tx ∧ function_on f X Y) (∀y : set, y ∈ Y → ∃x : set, x ∈ X ∧ apply_fun f x = y) Hf).

We prove the intermediate claim HTx: topology_on X Tx.

An exact proof term for the current goal is (andEL (topology_on X Tx) (function_on f X Y) Htopfun).

We prove the intermediate claim Hf_on: function_on f X Y.

An exact proof term for the current goal is (andER (topology_on X Tx) (function_on f X Y) Htopfun).

Apply andI to the current goal.

An exact proof term for the current goal is HTx.

An exact proof term for the current goal is HTy.

An exact proof term for the current goal is Hf_on.

Let V be given.

Assume HV: V ∈ Ty.

We will prove preimage_of X f V ∈ Tx.

We prove the intermediate claim HVQ: V ∈ quotient_topology X Tx Y f.

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

An exact proof term for the current goal is (SepE2 (𝒫 Y) (λV0 : set ⇒ preimage_of X f V0 ∈ Tx) V HVQ).

∎