proposition: Lemma disjoint_comp : forall A A' B B' : part_set E, Equal A A' -> Equal B B' -> disjoint A B -> disjoint A' B'.
proof: Proof. unfold disjoint in |- *. intros A A' B B' H' H'0 H'1; try assumption. apply Trans with (inter A B). auto with *. auto with *. Qed.
imports: Fpart Inter Arith