proposition: Lemma filter_from_basis_basis: filter_basis Build_Filter_from_basis B.
proof: Proof. constructor. - simpl. red; intros S ?. constructor. exists S; split; auto with sets. - intros. simpl in H. destruct H. exact H. Qed.
imports: ZornsLemma(DecidableDec FiniteIntersections FunctionProperties)