--- a/src/HOL/Real/HahnBanach/ZornLemma.thy Wed Jun 13 19:14:51 2007 +0200
+++ b/src/HOL/Real/HahnBanach/ZornLemma.thy Thu Jun 14 00:22:45 2007 +0200
@@ -48,6 +48,7 @@
show "\<Union>c \<in> S"
proof (rule r)
from c show "\<exists>x. x \<in> c" by fast
+ show "c \<in> chain S" by fact
qed
qed
qed