proposition: Lemma cardinal_Im_intro : forall (A:Ensemble U) (f:U -> V) (n:nat), cardinal _ A n -> exists p : nat, cardinal _ (Im A f) p.
proof: Proof. intros. apply finite_cardinal; apply finite_image. apply cardinal_finite with n; trivial with sets. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts Finite_sets_facts