Let X, T, T' and Y be given.
Assume Htop: topology_on X T.
Assume Htop': topology_on X T'.
Assume Hfiner: T' ⊆ T.
Assume HY: Y ⊆ X.
We will prove subspace_topology X T' Y ⊆ subspace_topology X T Y.
Let W be given.
Assume HW: W ∈ subspace_topology X T' Y.
We will prove W ∈ subspace_topology X T Y.
We prove the intermediate claim HWPowerY: W ∈ 𝒫 Y.
An exact proof term for the current goal is (subspace_topology_in_Power X T' Y W HW).
We prove the intermediate claim HWexists: ∃V ∈ T', W = V ∩ Y.
An exact proof term for the current goal is (subspace_topologyE X T' Y W HW).
Apply HWexists to the current goal.
Let V' be given.
Assume HV': V' ∈ T' ∧ W = V' ∩ Y.
We prove the intermediate claim HV'inT': V' ∈ T'.
An exact proof term for the current goal is (andEL (V' ∈ T') (W = V' ∩ Y) HV').
We prove the intermediate claim HWeqV'Y: W = V' ∩ Y.
An exact proof term for the current goal is (andER (V' ∈ T') (W = V' ∩ Y) HV').
We prove the intermediate claim HV'inT: V' ∈ T.
An exact proof term for the current goal is (Hfiner V' HV'inT').
We prove the intermediate claim HWPred: ∃V ∈ T, W = V ∩ Y.
We use V' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HV'inT.
An exact proof term for the current goal is HWeqV'Y.
An exact proof term for the current goal is (SepI (𝒫 Y) (λW0 : set ⇒ ∃V ∈ T, W0 = V ∩ Y) W HWPowerY HWPred).
∎