for T, S being TopSpace
for f being Function of T,S holds
( f is open iff ex B being Basis of T st
for V being Subset of T st V in B holds
f .: V is open )