feat(Mathlib/Topology/Bases): Subbasis closed under intersection

[mans0954]

We show that if a sub basis is closed under finite intersections and contains the universal set then it is a basis for a topology.

As a corollary, if a sub basis is closed under finite intersections, then inserting the empty set gives a basis for the topology.

An example application of this result is given in #12234

---