proposition: Lemma Disjoint_Intersection: forall (A : Type) (s1 s2 : Ensemble A), Disjoint s1 s2 <-> Intersection s1 s2 = Empty_set.
proof: Proof. intros. split. - apply Coq.Sets.Powerset_facts.Disjoint_Intersection. - intros. constructor. intros. intros ?. rewrite H in H0. destruct H0. Qed.
imports: ZornsLemma(FunctionProperties) Coq(RelationClasses)