proposition: Lemma Im_inv : forall (X:Ensemble U) (f:U -> V) (y:V), In _ (Im X f) y -> exists x : U, In _ X x /\ f x = y.
proof: Proof. intros X f y H'; elim H'. intros x H'0 y0 H'1; rewrite H'1. exists x; auto with sets. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts Finite_sets_facts