--- a/src/HOL/Product_Type.thy Wed Oct 17 07:50:46 2018 +0200
+++ b/src/HOL/Product_Type.thy Wed Oct 17 14:19:07 2018 +0100
@@ -1100,6 +1100,9 @@
lemma Times_empty [simp]: "A \<times> B = {} \<longleftrightarrow> A = {} \<or> B = {}"
by auto
+lemma times_subset_iff: "A \<times> C \<subseteq> B \<times> D \<longleftrightarrow> A={} \<or> C={} \<or> A \<subseteq> B \<and> C \<subseteq> D"
+ by blast
+
lemma times_eq_iff: "A \<times> B = C \<times> D \<longleftrightarrow> A = C \<and> B = D \<or> (A = {} \<or> B = {}) \<and> (C = {} \<or> D = {})"
by auto