theorem Th9: :: YELLOW_8:9

for T being TopStruct
for B being Basis of T
for V being Subset of T st V is open holds
V = union { G where G is Subset of T : ( G in B & G c= V ) }