proposition: Lemma included_comp : forall A A' B B' : part_set E, Equal A A' -> Equal B B' -> included A B -> included A' B'.
proof: Proof. simpl in |- *; unfold eq_part, included in |- *. intros A A' B B' H' H'0 H'1 x H'2; try assumption. elim (H'0 x); intros H'4 H'5; apply H'4. lapply (H'1 x); [ intros H'6; apply H'6 | idtac ]. elim (H' x); intros H'6 H'7; apply H'7; auto with algebra. Qed.
imports: Sets