proposition: Lemma union_part_upper_bound : forall Y : part_set E, (forall A : part_set E, in_part A P -> included A Y) -> included union_part Y.
proof: Proof. intros Y H'; try assumption. unfold included in |- *. intros x H'0; try assumption. case (union_part_prop H'0). intros A H'1; try assumption. elim H'1. intros H'2 H'3; try assumption. unfold included in H'. apply H' with (A := A); auto with algebra. Qed.
imports: Sets