for T being non empty TopStruct
for B being Basis of T
for V being Subset of T st V is open & V <> {} holds
ex W being Subset of T st
( W in B & W c= V & W <> {} )