proposition: Lemma inter_union : forall A B C : Ensf, inter A C empty -> inter B C empty -> inter (union A B) C empty.
proof: Proof. unfold inter in |- *. intros. elim H0; clear H0. intros H0 H1; elim H1; clear H1; intros H1 H2. elim H; clear H. intros H3 H4; elim H4; clear H4; intros H4 H5. split; auto. split; auto. intros. cut (dans x A \/ dans x B); auto. intro H7; elim H7; auto. Qed.
imports: Ensf_types Ensf_dans Ensf_union Ensf_inclus