[STATEMENT]
lemma (in bounded_lattice_bot) atomic_implies_join_prime:
  assumes "atomic x"
  shows "join_irreducible x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. join_irreducible x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
atomic x

goal (1 subgoal):
 1. join_irreducible x
[PROOF STEP]
unfolding 
    atomic_def 
    join_irreducible_def'
[PROOF STATE]
proof (prove)
using this:
x \<noteq> \<bottom> \<and> (\<forall>y\<le>x. y = \<bottom> \<or> y = x)

goal (1 subgoal):
 1. x \<noteq> \<bottom> \<and> (\<forall>y z. x = y \<squnion> z \<longrightarrow> x = y \<or> x = z)
[PROOF STEP]
by (metis (no_types, opaque_lifting) 
        sup.cobounded2 
        sup_bot.right_neutral)