[STATEMENT]
lemma dual_downsets: "downsets = dual_ord.upsets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. downsets = ord.upsets (\<lambda>x y. y \<le> x)
[PROOF STEP]
by (simp add: dual_ord.dual_upsets)