theorem Th1: :: TOPGEN_2:1

for T being non empty TopSpace
for B being Basis of T
for x being Element of T holds { U where U is Subset of T : ( x in U & U in B ) } is Basis of x