proposition: Lemma surj_part_image_surjective : forall A : part_set E, surjective (surj_part_image A).
proof: Proof. red in |- *. intros A y; try assumption. case (image_in (subtype_prf y)). intros x H'; try assumption. elim H'; intros H'0 H'1; try exact H'1; clear H'. exists (Build_subtype H'0); try assumption. Qed.
imports: Classical_Prop Parts