[STATEMENT]
lemma bottom_below_in:
  "has_bottom P \<Longrightarrow> x\<in>P \<Longrightarrow> bottom (P.\<^bold>\<le>x) = bottom P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has_bottom P; x \<in> P\<rbrakk> \<Longrightarrow> bottom (P .\<^bold>\<le> x) = bottom P
[PROOF STEP]
using bottom_in_below_in
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>has_bottom ?P; ?x \<in> ?P\<rbrakk> \<Longrightarrow> bottom ?P \<in> ?P .\<^bold>\<le> ?x

goal (1 subgoal):
 1. \<lbrakk>has_bottom P; x \<in> P\<rbrakk> \<Longrightarrow> bottom (P .\<^bold>\<le> x) = bottom P
[PROOF STEP]
by (fast intro: bottomI[THEN sym])