proposition: Lemma invimage_image : forall A : part_set F, included (image f (invimage f A)) A.
proof: Proof. unfold included in |- *. simpl in |- *; auto with algebra. intros A x H'; try assumption. elim H'; intros x0 E0; elim E0; intros H'0 H'1; try exact H'1; clear E0 H'. apply in_part_comp_l with (Ap f x0); auto with algebra. Qed.
imports: Parts2