removed unused lemma chain_mono2

--- a/src/HOLCF/Pcpo.thy	Wed Nov 10 11:42:35 2010 -0800
+++ b/src/HOLCF/Pcpo.thy	Wed Nov 10 13:08:42 2010 -0800
@@ -238,9 +238,6 @@
 lemma notUU_I: "\<lbrakk>x \<sqsubseteq> y; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> y \<noteq> \<bottom>"
   by (blast intro: UU_I)
 
-lemma chain_mono2: "\<lbrakk>\<exists>j. Y j \<noteq> \<bottom>; chain Y\<rbrakk> \<Longrightarrow> \<exists>j. \<forall>i>j. Y i \<noteq> \<bottom>"
-  by (blast dest: notUU_I chain_mono_less)
-
 end
 
 subsection {* Chain-finite and flat cpos *}