for T being non empty TopStruct
for x being Point of T
for B being Basis of x
for V being Subset of T st x in V & V is open holds
ex W being Subset of T st
( W in B & W c= V ) by Def1;