proposition: Lemma Disjoint_Included_Complement : forall (A : Type) (s1 s2 : Ensemble A), Disjoint s1 s2 <-> Included s1 (Complement s2).
proof: Proof. intros. split. - intros. intros ? ? ?. destruct H. apply (H x). split; assumption. - intros. constructor. intros ? ?. destruct H0. apply (H x); assumption. Qed.
imports: ZornsLemma(FunctionProperties) Coq(RelationClasses)