--- a/src/HOL/Analysis/Elementary_Topology.thy Wed Nov 06 16:38:58 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy Wed Nov 06 17:38:19 2019 +0100
@@ -16,11 +16,6 @@
section \<open>Elementary Topology\<close>
-subsection \<open>TODO: move?\<close>
-
-lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)"
- using openI by auto
-
subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Affine transformations of intervals\<close>
@@ -49,7 +44,6 @@
by (simp add: field_simps)
-
subsection \<open>Topological Basis\<close>
context topological_space