proposition: Lemma eq_part_included : forall A B : part_set E, Equal A B -> included A B.
proof: Proof. simpl in |- *; unfold eq_part, included in |- *. intros A B H' x H'0; try assumption. specialize H' with (x := x); rename H' into H'1; try exact H'1. elim H'1; intros H'2 H'3; try exact H'2; clear H'1; auto with algebra. Qed.
imports: Sets