for X being non empty TopSpace
for U1 being Subset of X holds
( U1 is open iff for x being Point of X st x in U1 holds
ex A being Subset of X st
( A is a_neighborhood of x & A c= U1 ) )