diff -r b3956a37c994 -r d628bbdce79a src/HOL/Analysis/Elementary_Topology.thy
--- 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