diff -r b93d1b3ee300 -r bd91b77c4cd6 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Aug 28 16:28:07 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Aug 28 20:56:49 2011 -0700
@@ -220,6 +220,25 @@
   unfolding euclidean_component_def
   by (rule order_trans [OF Cauchy_Schwarz_ineq2]) simp
 
+subsection {* Subclass relationships *}
+
+instance euclidean_space \<subseteq> perfect_space
+proof
+  fix x :: 'a show "\<not> open {x}"
+  proof
+    assume "open {x}"
+    then obtain e where "0 < e" and e: "\<forall>y. dist y x < e \<longrightarrow> y = x"
+      unfolding open_dist by fast
+    def y \<equiv> "x + scaleR (e/2) (sgn (basis 0))"
+    from `0 < e` have "y \<noteq> x"
+      unfolding y_def by (simp add: sgn_zero_iff DIM_positive)
+    from `0 < e` have "dist y x < e"
+      unfolding y_def by (simp add: dist_norm norm_sgn)
+    from `y \<noteq> x` and `dist y x < e` show "False"
+      using e by simp
+  qed
+qed
+
 subsection {* Class instances *}
 
 subsubsection {* Type @{typ real} *}