src/HOL/Set.thy
changeset 14335 9c0b5e081037
parent 14302 6c24235e8d5d
child 14381 1189a8212a12
--- a/src/HOL/Set.thy	Thu Jan 01 10:06:32 2004 +0100
+++ b/src/HOL/Set.thy	Thu Jan 01 21:47:07 2004 +0100
@@ -868,6 +868,16 @@
 lemma psubset_imp_subset: "A \<subset> B ==> A \<subseteq> B"
   by (simp add: psubset_eq)
 
+lemma psubset_trans: "[| A \<subset> B; B \<subset> C |] ==> A \<subset> C"
+apply (unfold psubset_def)
+apply (auto dest: subset_antisym)
+done
+
+lemma psubsetD: "[| A \<subset> B; c \<in> A |] ==> c \<in> B"
+apply (unfold psubset_def)
+apply (auto dest: subsetD)
+done
+
 lemma psubset_subset_trans: "A \<subset> B ==> B \<subseteq> C ==> A \<subset> C"
   by (auto simp add: psubset_eq)