for T being TopSpace
for B being Subset-Family of T st B c= the topology of T & ( for A being Subset of T st A is open holds
for p being Point of T st p in A holds
ex a being Subset of T st
( a in B & p in a & a c= A ) ) holds
B is Basis of T