We will prove ∃Tsmall Tall : set, topology_on abc_set Tsmall ∧ topology_on abc_set Tall.

We use (indiscrete_topology abc_set) to witness the existential quantifier.

We use (discrete_topology abc_set) to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (indiscrete_topology_on abc_set).

An exact proof term for the current goal is (discrete_topology_on abc_set).

∎