# HG changeset patch
# User huffman
# Date 1272502139 25200
# Node ID 1535841fc2e981ca35d40d3e2fa27f9c55c925cb
# Parent  68ce5760c585ffb3a54826a55747d11cdae7c43b
prove lemma openin_subopen without using choice

diff -r 68ce5760c585 -r 1535841fc2e9 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Apr 28 16:11:07 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Apr 28 17:48:59 2010 -0700
@@ -66,16 +66,14 @@
 lemma openin_topspace[intro, simp]: "openin U (topspace U)" by (simp add: openin_Union topspace_def)
 
 lemma openin_subopen: "openin U S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>T. openin U T \<and> x \<in> T \<and> T \<subseteq> S)" (is "?lhs \<longleftrightarrow> ?rhs")
-proof-
-  {assume ?lhs then have ?rhs by auto }
-  moreover
-  {assume H: ?rhs
-    then obtain t where t: "\<forall>x\<in>S. openin U (t x) \<and> x \<in> t x \<and> t x \<subseteq> S"
-      unfolding Ball_def ex_simps(6)[symmetric] choice_iff by blast
-    from t have th0: "\<forall>x\<in> t`S. openin U x" by auto
-    have "\<Union> t`S = S" using t by auto
-    with openin_Union[OF th0] have "openin U S" by simp }
-  ultimately show ?thesis by blast
+proof
+  assume ?lhs then show ?rhs by auto
+next
+  assume H: ?rhs
+  let ?t = "\<Union>{T. openin U T \<and> T \<subseteq> S}"
+  have "openin U ?t" by (simp add: openin_Union)
+  also have "?t = S" using H by auto
+  finally show "openin U S" .
 qed
 
 subsection{* Closed sets *}