let S, T be non empty TopSpace; :: thesis: for f being Function of S,T st f is being_homeomorphism holds

f " is open

let f be Function of S,T; :: thesis: ( f is being_homeomorphism implies f " is open )

assume f is being_homeomorphism ; :: thesis: f " is open

then A1: ( rng f = [#] T & f is one-to-one & f is continuous ) by TOPS_2:def 5;

let P be Subset of T; :: according to T_0TOPSP:def 2 :: thesis: ( not P is open or (f ") .: P is open )

f " P = (f ") .: P by A1, TOPS_2:55;

hence ( not P is open or (f ") .: P is open ) by A1, TOPS_2:43; :: thesis: verum

f " is open

let f be Function of S,T; :: thesis: ( f is being_homeomorphism implies f " is open )

assume f is being_homeomorphism ; :: thesis: f " is open

then A1: ( rng f = [#] T & f is one-to-one & f is continuous ) by TOPS_2:def 5;

let P be Subset of T; :: according to T_0TOPSP:def 2 :: thesis: ( not P is open or (f ") .: P is open )

f " P = (f ") .: P by A1, TOPS_2:55;

hence ( not P is open or (f ") .: P is open ) by A1, TOPS_2:43; :: thesis: verum