Let X be given.
We will prove indiscrete_topology X ⊆ countable_complement_topology X.
Let U be given.
Assume HU: U ∈ indiscrete_topology X.
Apply UPairE U Empty X HU to the current goal.
Assume HUempty: U = Empty.
rewrite the current goal using HUempty (from left to right).
An exact proof term for the current goal is (countable_complement_topology_contains_empty X).
Assume HUX: U = X.
rewrite the current goal using HUX (from left to right).
An exact proof term for the current goal is (countable_complement_topology_contains_full X).
∎