theorem :: TOPGRP_1:26

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