Let X, Tx and A be given.

Assume HX: completely_normal_space X Tx.

Assume HA: A ⊆ X.

We will prove completely_normal_space A (subspace_topology X Tx A).

We prove the intermediate claim HTx: topology_on X Tx.

An exact proof term for the current goal is (andEL (topology_on X Tx) (∀Y : set, Y ⊆ X → normal_space Y (subspace_topology X Tx Y)) HX).

We prove the intermediate claim HallCN: ∀Y : set, Y ⊆ X → normal_space Y (subspace_topology X Tx Y).

An exact proof term for the current goal is (andER (topology_on X Tx) (∀Y : set, Y ⊆ X → normal_space Y (subspace_topology X Tx Y)) HX).

We will prove topology_on A (subspace_topology X Tx A) ∧ ∀Y : set, Y ⊆ A → normal_space Y (subspace_topology A (subspace_topology X Tx A) Y).

Apply andI to the current goal.

An exact proof term for the current goal is (subspace_topology_is_topology X Tx A HTx HA).

Let Y be given.

Assume HY: Y ⊆ A.

We will prove normal_space Y (subspace_topology A (subspace_topology X Tx A) Y).

We prove the intermediate claim HYsubX: Y ⊆ X.

An exact proof term for the current goal is (Subq_tra Y A X HY HA).

We prove the intermediate claim Hsubeq: subspace_topology A (subspace_topology X Tx A) Y = subspace_topology X Tx Y.

An exact proof term for the current goal is (ex16_1_subspace_transitive X Tx A Y HTx HA HY).

rewrite the current goal using Hsubeq (from left to right).

An exact proof term for the current goal is (HallCN Y HYsubX).

Let X, Tx, Y and Ty be given.

Assume HX: completely_normal_space X Tx.

Assume HY: completely_normal_space Y Ty.

An exact proof term for the current goal is (xm (completely_normal_space (setprod X Y) (product_topology X Tx Y Ty))).

Let X be given.

Assume Hwo: well_ordered_set X.

Assume Hso: simply_ordered_set X.

An exact proof term for the current goal is (xm (completely_normal_space X (order_topology X))).

Let X and Tx be given.

Assume Hmet: metrizable X Tx.

We will prove completely_normal_space X Tx.

We will prove topology_on X Tx ∧ (∀Y : set, Y ⊆ X → normal_space Y (subspace_topology X Tx Y)).

Apply andI to the current goal.

Apply Hmet to the current goal.

Let d be given.

Assume HdPair: metric_on X d ∧ metric_topology X d = Tx.

We prove the intermediate claim Hd: metric_on X d.

An exact proof term for the current goal is (andEL (metric_on X d) (metric_topology X d = Tx) HdPair).

We prove the intermediate claim Heq: metric_topology X d = Tx.

An exact proof term for the current goal is (andER (metric_on X d) (metric_topology X d = Tx) HdPair).

We prove the intermediate claim HTm: topology_on X (metric_topology X d).

An exact proof term for the current goal is (metric_topology_is_topology X d Hd).

rewrite the current goal using Heq (from right to left).

An exact proof term for the current goal is HTm.

Let Y be given.

Assume HY: Y ⊆ X.

We prove the intermediate claim HmetY: metrizable Y (subspace_topology X Tx Y).

An exact proof term for the current goal is (subspace_of_metrizable_is_metrizable X Tx Y Hmet HY).

An exact proof term for the current goal is (supp_ex_locally_euclidean_2_iii_implies_iv Y (subspace_topology X Tx Y) HmetY).

Let X and Tx be given.

Assume Hc: compact_space X Tx.

Assume HH: Hausdorff_space X Tx.

An exact proof term for the current goal is (xm (completely_normal_space X Tx)).

Let X and Tx be given.

Assume Hr: regular_space X Tx.

Assume Hsc: second_countable_space X Tx.

An exact proof term for the current goal is (xm (completely_normal_space X Tx)).

An exact proof term for the current goal is (xm (completely_normal_space R R_lower_limit_topology)).