Let X, Tx and Y be given.
Assume HTx: topology_on X Tx.
Assume HY: Y ⊆ X.
Assume HT1: T1_space X Tx.
We will prove T1_space Y (subspace_topology X Tx Y).
We prove the intermediate claim HTy: topology_on Y (subspace_topology X Tx Y).
An exact proof term for the current goal is (subspace_topology_is_topology X Tx Y HTx HY).
Apply (iffER (T1_space Y (subspace_topology X Tx Y)) (∀y : set, y ∈ Y → closed_in Y (subspace_topology X Tx Y) {y}) (lemma_T1_singletons_closed Y (subspace_topology X Tx Y) HTy)) to the current goal.
We will prove ∀y : set, y ∈ Y → closed_in Y (subspace_topology X Tx Y) {y}.
Let y be given.
Assume HyY: y ∈ Y.
We will prove closed_in Y (subspace_topology X Tx Y) {y}.
Apply (iffER (closed_in Y (subspace_topology X Tx Y) {y}) (∃C : set, closed_in X Tx C ∧ {y} = C ∩ Y) (closed_in_subspace_iff_intersection X Tx Y {y} HTx HY)) to the current goal.
We use {y} to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is ((iffEL (T1_space X Tx) (∀z : set, z ∈ X → closed_in X Tx {z}) (lemma_T1_singletons_closed X Tx HTx) HT1) y (HY y HyY)).
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ {y}.
We will prove z ∈ {y} ∩ Y.
We prove the intermediate claim Hzeq: z = y.
An exact proof term for the current goal is (SingE y z Hz).
rewrite the current goal using Hzeq (from left to right).
An exact proof term for the current goal is (binintersectI {y} Y y (SingI y) HyY).
Let z be given.
Assume Hz: z ∈ {y} ∩ Y.
We will prove z ∈ {y}.
An exact proof term for the current goal is (binintersectE1 {y} Y z Hz).
∎