src/HOL/Set.thy
changeset 14335 9c0b5e081037
parent 14302 6c24235e8d5d
child 14381 1189a8212a12
     1.1 --- a/src/HOL/Set.thy	Thu Jan 01 10:06:32 2004 +0100
     1.2 +++ b/src/HOL/Set.thy	Thu Jan 01 21:47:07 2004 +0100
     1.3 @@ -868,6 +868,16 @@
     1.4  lemma psubset_imp_subset: "A \<subset> B ==> A \<subseteq> B"
     1.5    by (simp add: psubset_eq)
     1.6  
     1.7 +lemma psubset_trans: "[| A \<subset> B; B \<subset> C |] ==> A \<subset> C"
     1.8 +apply (unfold psubset_def)
     1.9 +apply (auto dest: subset_antisym)
    1.10 +done
    1.11 +
    1.12 +lemma psubsetD: "[| A \<subset> B; c \<in> A |] ==> c \<in> B"
    1.13 +apply (unfold psubset_def)
    1.14 +apply (auto dest: subsetD)
    1.15 +done
    1.16 +
    1.17  lemma psubset_subset_trans: "A \<subset> B ==> B \<subseteq> C ==> A \<subset> C"
    1.18    by (auto simp add: psubset_eq)
    1.19