let S, T be non empty TopSpace; :: thesis: for f being Function of S,T st f is one-to-one & f is onto & f is continuous & f is open holds
f is being_homeomorphism
let f be Function of S,T; :: thesis: ( f is one-to-one & f is onto & f is continuous & f is open implies f is being_homeomorphism )
assume that
A1: f is one-to-one and
A2: f is onto and
A3: f is continuous and
A4: f is open ; :: thesis: f is being_homeomorphism
A5: [#] T <> {} ;
A6: dom f = the carrier of S by FUNCT_2:def 1;
A7: for P being Subset of S holds
( P is open iff f .: P is open )

proof

let P be Subset of S; :: thesis: ( P is open iff f .: P is open )
thus ( P is open implies f .: P is open ) by A4; :: thesis: ( f .: P is open implies P is open )
assume f .: P is open ; :: thesis: P is open
then f " (f .: P) is open by A3, A5, TOPS_2:43;
hence P is open by A1, A6, FUNCT_1:94; :: thesis: verum

end;

( dom f = [#] S & rng f = [#] T ) by A2, FUNCT_2:def 1;
hence f is being_homeomorphism by A1, A7, TOPGRP_1:25; :: thesis: verum