We prove the intermediate claim HcontAll: finer_than R_upper_limit_topology R_standard_topology ∧ finer_than R_K_topology R_standard_topology ∧ finer_than R_standard_topology R_finite_complement_topology ∧ finer_than R_standard_topology R_ray_topology.
An exact proof term for the current goal is ex13_7_R_topology_containments.
We prove the intermediate claim Hleft1: (finer_than R_upper_limit_topology R_standard_topology ∧ finer_than R_K_topology R_standard_topology) ∧ finer_than R_standard_topology R_finite_complement_topology.
An exact proof term for the current goal is (andEL ((finer_than R_upper_limit_topology R_standard_topology ∧ finer_than R_K_topology R_standard_topology) ∧ finer_than R_standard_topology R_finite_complement_topology) (finer_than R_standard_topology R_ray_topology) HcontAll).
We prove the intermediate claim Hleft2: finer_than R_upper_limit_topology R_standard_topology ∧ finer_than R_K_topology R_standard_topology.
An exact proof term for the current goal is (andEL (finer_than R_upper_limit_topology R_standard_topology ∧ finer_than R_K_topology R_standard_topology) (finer_than R_standard_topology R_finite_complement_topology) Hleft1).
We prove the intermediate claim Hsub: R_standard_topology ⊆ R_K_topology.
An exact proof term for the current goal is (andER (finer_than R_upper_limit_topology R_standard_topology) (finer_than R_K_topology R_standard_topology) Hleft2).
An exact proof term for the current goal is (finer_preserves_Hausdorff R R_standard_topology R_K_topology R_standard_topology_Hausdorff R_K_topology_is_topology_local Hsub).
∎