[STATEMENT]
lemma cdsi:"d O s^-1 \<subseteq> b^-1 \<union> m^-1 \<union> ov^-1 \<union> f \<union> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d O s\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse> \<union> f \<union> d
[PROOF STEP]
using csdi
[PROOF STATE]
proof (prove)
using this:
s O d\<inverse> \<subseteq> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>

goal (1 subgoal):
 1. d O s\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse> \<union> f \<union> d
[PROOF STEP]
by auto