[STATEMENT]
lemma constrains_Int: 
    "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<inter> B) co (A' \<inter> B')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<in> A co A'; F \<in> B co B'\<rbrakk> \<Longrightarrow> F \<in> A \<inter> B co A' \<inter> B'
[PROOF STEP]
by (unfold constrains_def, blast)