[STATEMENT]
lemma dual_up_closed:
  "up_closed x \<longleftrightarrow> up_closed (x\<^sup>d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. up_closed x = up_closed (x\<^sup>d)
[PROOF STEP]
by (metis dual_involutive dual_one up_closed_def strong_up_closed_2)