:: deftheorem defines open T_0TOPSP:def 2 :
for T, S being TopStruct
for f being Function of T,S holds
( f is open iff for A being Subset of T st A is open holds
f .: A is open );