[STATEMENT]
lemma meet_ord: "ad x \<le> ad y \<longleftrightarrow> ad x \<cdot> ad y = ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ad x \<le> ad y) = (ad x \<cdot> ad y = ad x)
[PROOF STEP]
by (metis a_d_closed a_subid_aux d1_a order.antisym mult_1_right mult_isol)