src/ZF/ZF.thy

      "A<=B <-> (\<forall>x. x\<in>A \<longrightarrow> x\<in>B)"
 apply (unfold subset_def Ball_def)
 apply (rule iff_refl)
 done
 
+text{*For calculations*}
+declare subsetD [trans] rev_subsetD [trans] subset_trans [trans]
+
 
 subsection{*Rules for equality*}
 
 (*Anti-symmetry of the subset relation*)
 lemma equalityI [intro]: "[| A \<subseteq> B;  B \<subseteq> A |] ==> A = B"