proposition: Lemma image_invimage : forall A : part_set E, included A (invimage f (image f A)).
proof: Proof. unfold included in |- *. simpl in |- *; auto with algebra. intros A x H'; exists x; split; [ try assumption | idtac ]; auto with algebra. Qed.
imports: Parts2