src/HOL/Set.thy
changeset 14551 2cb6ff394bfb
parent 14479 0eca4aabf371
child 14565 c6dc17aab88a
     1.1 --- a/src/HOL/Set.thy	Tue Apr 13 07:48:32 2004 +0200
     1.2 +++ b/src/HOL/Set.thy	Tue Apr 13 09:42:40 2004 +0200
     1.3 @@ -943,6 +943,10 @@
     1.4  lemma Inter_lower: "B \<in> A ==> Inter A \<subseteq> B"
     1.5    by blast
     1.6  
     1.7 +lemma Inter_subset:
     1.8 +  "[| !!X. X \<in> A ==> X \<subseteq> B; A ~= {} |] ==> \<Inter>A \<subseteq> B"
     1.9 +  by blast
    1.10 +
    1.11  lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A"
    1.12    by (rules intro: InterI subsetI dest: subsetD)
    1.13