[STATEMENT]
lemma lm031: 
  "{a. Domain a \<subseteq> N    &   Range a \<in> all_partitions G} =
   (Domain -`(Pow N))  \<inter>  (Range -` (all_partitions G)) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a. Domain a \<subseteq> N \<and> Range a \<in> all_partitions G} = Domain -` Pow N \<inter> Range -` all_partitions G
[PROOF STEP]
by fastforce