Let A, B, X and Tx be given.
Assume HTx: topology_on X Tx.
Assume HAB: A ⊆ B.
Assume HBX: B ⊆ X.
Assume HdA: dense_in A X Tx.
We will prove dense_in B X Tx.
We will prove closure_of X Tx B = X.
Apply set_ext to the current goal.
An exact proof term for the current goal is (closure_in_space X Tx B HTx).
Let x be given.
Assume HxX: x ∈ X.
We will prove x ∈ closure_of X Tx B.
We prove the intermediate claim HclMono: closure_of X Tx A ⊆ closure_of X Tx B.
An exact proof term for the current goal is (closure_monotone X Tx A B HTx HAB HBX).
We prove the intermediate claim HdAeq: closure_of X Tx A = X.
An exact proof term for the current goal is HdA.
We prove the intermediate claim HxclA: x ∈ closure_of X Tx A.
rewrite the current goal using HdAeq (from left to right).
An exact proof term for the current goal is HxX.
An exact proof term for the current goal is (HclMono x HxclA).
∎