[STATEMENT]
lemma \<alpha>_strict[simp]: "\<alpha> bot = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> bot = bot
[PROOF STEP]
using \<alpha>_dist[of "{}"]
[PROOF STATE]
proof (prove)
using this:
is_chain {} \<Longrightarrow> \<alpha> (Sup {}) = Sup (\<alpha> ` {})

goal (1 subgoal):
 1. \<alpha> bot = bot
[PROOF STEP]
by simp