[STATEMENT]
lemma bot_annirr'' [simp]: "x \<cdot> \<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<cdot> \<bottom> = \<bottom>
[PROOF STEP]
using Sup_distl[where Y="{}"]
[PROOF STATE]
proof (prove)
using this:
?x \<cdot> Sup {} = Sup {z. \<exists>y\<in>{}. z = ?x \<cdot> y}

goal (1 subgoal):
 1. x \<cdot> \<bottom> = \<bottom>
[PROOF STEP]
by auto