proposition: Lemma inter_comp : forall A A' B B' : part_set E, Equal A A' -> Equal B B' -> Equal (inter A B) (inter A' B').
proof: Proof. unfold inter in |- *; simpl in |- *. unfold eq_part in |- *; simpl in |- *. intros A A' B B' H' H'0 x. generalize (H' x) (H'0 x); tauto. Qed.
imports: Union