theorem Th4: :: TOPS_4:4
for T being non empty TopSpace
for M being non empty MetrSpace
for f being Function of T,(TopSpaceMetr M) holds
( f is open iff for p being Point of T
for V being open Subset of T
for q being Point of M st q = f . p & p in V holds
ex r being positive Real st Ball (q,r) c= f .: V )