proposition: Lemma filter_from_subbasis_subbasis: filter_subbasis Build_Filter_from_subbasis B.
proof: Proof. assert (filter_basis Build_Filter_from_subbasis (finite_intersections B)). { apply filter_from_basis_basis. } destruct H. constructor. - assert (Included B (finite_intersections B)); auto with sets. red; intros. constructor; trivial. - intros. destruct (filter_basis_cond0 S H) as [S' []]. pose proof (finite_intersection_is_finite_indexed_intersection _ _ H0). destruct H2 as [J [? [V []]]]. exists J; split; trivial. exists V; split; trivial. rewrite <- H4; trivial. Qed.
imports: ZornsLemma(DecidableDec FiniteIntersections FunctionProperties) ZornsLemma(FiniteIntersections)