[STATEMENT]
lemma cmfi:"m O f^-1 \<subseteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m O f\<inverse> \<subseteq> b
[PROOF STEP]
apply (r_compose r1:m r2:f r3:b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z k l u. \<lbrakk>x \<parallel> y; k \<parallel> l; l \<parallel> z; z \<parallel> u; k \<parallel> y; y \<parallel> u\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
by (meson M1)