theorem :: TOPS_2:58

for T being TopStruct
for S being non empty TopStruct
for f being Function of T,S holds
( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds
( P is closed iff f .: P is closed ) ) ) )