fact: Hypothesis neighborhood_basis_cond : forall (U V:Ensemble X) (x:X), In (NB x) U -> In (NB x) V -> exists W:Ensemble X, In (NB x) W /\ Included W (Intersection U V).
imports: TopologicalSpaces Neighborhoods OpenBases