proposition: Lemma union_part_included : forall A : part_set E, in_part A P -> included A union_part.
proof: Proof. intros A H'; try assumption. unfold included in |- *; auto with algebra. intros x H'0; try assumption. apply union_part_prop_rev with (A := A); auto with algebra. Qed.
imports: Sets