theorem Th31: :: YELLOW_9:31

for T being TopSpace
for B being Basis of T
for A being Subset of T holds
( A is open iff 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 ) )