theory Prelude+− imports Main+− begin+− +− (*+− To make the theory work under Isabelle 2009 and 2011+− +− Isabelle 2009: set_ext+− Isabelle 2011: set_eqI+− +− *)+− +− +− lemma set_eq_intro:+− "(\<And>x. (x \<in> A) = (x \<in> B)) \<Longrightarrow> A = B"+− by blast+− +− +− end+−