proposition: Lemma image_included : forall A B : part_set E, included A B -> included (image A) (image B).
proof: Proof. intros A B H'; try assumption. unfold included in |- *. intros x H'0; try assumption. elim H'0. intros x0 H'1; try assumption. apply in_image with (x := x0); auto with algebra. red in H'. elim H'1. auto with algebra. elim H'1; auto with algebra. Qed.
imports: Classical_Prop Parts