*)

 *)

 header {* Infinite Sets and Related Concepts *}

 header {* Infinite Sets and Related Concepts *}

 theory Infinite_Set

 theory Infinite_Set

 begin

 begin

 subsection "Infinite Sets"

 subsection "Infinite Sets"

 text {*

 text {*

 lemma atmost_one_unique [elim]: "atmost_one S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> y = x"

 lemma atmost_one_unique [elim]: "atmost_one S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> y = x"

   by (simp add: atmost_one_def)

   by (simp add: atmost_one_def)

 end

 end