proposition: Lemma open_basis_is_subbasis: open_basis SB -> subbasis.
proof: Proof. intros. destruct H. constructor. { exact open_basis_elements. } intros. destruct (open_basis_cover x U); trivial. destruct H1 as [? [? ?]]. exists x0. split; auto. split; auto. constructor. assumption. Qed.
imports: ZornsLemma(FiniteIntersections)