src/HOL/Complete_Lattice.thy
changeset 39302 d7728f65b353
parent 38705 aaee86c0e237
child 40714 4c17bfdf6f84
     1.1 --- a/src/HOL/Complete_Lattice.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Mon Sep 13 11:13:15 2010 +0200
     1.3 @@ -272,7 +272,7 @@
     1.4  
     1.5  lemma Union_eq:
     1.6    "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
     1.7 -proof (rule set_ext)
     1.8 +proof (rule set_eqI)
     1.9    fix x
    1.10    have "(\<exists>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<exists>B\<in>A. x \<in> B)"
    1.11      by auto
    1.12 @@ -508,7 +508,7 @@
    1.13  
    1.14  lemma Inter_eq:
    1.15    "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
    1.16 -proof (rule set_ext)
    1.17 +proof (rule set_eqI)
    1.18    fix x
    1.19    have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)"
    1.20      by auto