--- a/src/HOL/Analysis/Linear_Algebra.thy Thu Sep 15 14:33:55 2016 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy Thu Sep 15 15:48:37 2016 +0100
@@ -3125,6 +3125,9 @@
definition collinear :: "'a::real_vector set \<Rightarrow> bool"
where "collinear S \<longleftrightarrow> (\<exists>u. \<forall>x \<in> S. \<forall> y \<in> S. \<exists>c. x - y = c *\<^sub>R u)"
+lemma collinear_subset: "\<lbrakk>collinear T; S \<subseteq> T\<rbrakk> \<Longrightarrow> collinear S"
+ by (meson collinear_def subsetCE)
+
lemma collinear_empty [iff]: "collinear {}"
by (simp add: collinear_def)