[STATEMENT]
lemma upset_set_downset_set_dual: "(`) \<partial> \<circ> \<Up> = \<Down> \<circ> (`) \<partial>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (`) \<partial> \<circ> \<Up> = \<Down> \<circ> (`) \<partial>
[PROOF STEP]
unfolding downset_set_def upset_set_def fun_eq_iff comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. \<partial> ` {y. \<exists>x\<in>x. x \<le> y} = {y. Bex (\<partial> ` x) ((\<le>) y)}
[PROOF STEP]
apply (safe, force simp: dual_anti)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb xc. \<lbrakk>xa \<le> \<partial> xc; xc \<in> x\<rbrakk> \<Longrightarrow> xa \<in> \<partial> ` {y. \<exists>x\<in>x. x \<le> y}
[PROOF STEP]
by (metis (mono_tags, lifting) dual.exhaust dual_anti_iff mem_Collect_eq rev_image_eqI)