[STATEMENT]
lemma cka_1: "(x \<cdot> y)\<^sup>\<star> \<le> x\<^sup>\<star> \<cdot> y\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<cdot> y)\<^sup>\<star> \<le> x\<^sup>\<star> \<cdot> y\<^sup>\<star>
[PROOF STEP]
by (metis conway_c3 star_invol star_iso star_subdist_var_2)