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