proposition: Lemma image_empty : forall f:U -> V, Im (Empty_set U) f = Empty_set V.
proof: Proof. intro f; try assumption. apply Extensionality_Ensembles. split; auto with sets. red. intros x H'; elim H'. intros x0 H'0; elim H'0; auto with sets. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts Finite_sets_facts