proposition: Lemma disjoint_inclus : forall A B C : part_set E, included A B -> disjoint B C -> disjoint A C.
proof: Proof. unfold included, disjoint in |- *. intros A B C H' H'0; try assumption. apply not_in_empty. unfold not in |- *; intros. cut (in_part x (inter B C)). generalize (empty_not_in (A:=inter B C) H'0). unfold not in |- *; intros. apply H0 with (x := x). auto with *. auto with *. apply in_part_inter. apply H'. apply in_part_inter_l with C. auto with *. apply in_part_inter_r with A. auto with *. Qed.
imports: Fpart Inter Arith