proposition: Lemma disjoint_not_in_r : forall (A B : part_set E) (x : E), disjoint A B -> in_part x A -> ~ in_part x B.
proof: Proof. unfold disjoint in |- *. unfold not in |- *; intros. cut (in_part x (empty E)). auto with *. apply in_part_comp_r with (inter A B). auto with *. auto with *. Qed.
imports: Fpart Inter Arith