slightly more robust proof

--- a/src/HOL/Algebra/Lattice.thy	Mon Oct 11 08:32:09 2010 -0700
+++ b/src/HOL/Algebra/Lattice.thy	Tue Oct 12 21:30:44 2010 +0200
@@ -233,9 +233,8 @@
   assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
     and AA': "A {.=} A'"
   shows "Lower L A = Lower L A'"
-using Lower_memD[of y]
 unfolding Lower_def
-apply safe
+apply rule
  apply clarsimp defer 1
  apply clarsimp defer 1
 proof -