let T be TopSpace; :: thesis: for S being non empty TopSpace
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 f .: (Cl P) = Cl (f .: P) ) ) )
let S be non empty TopSpace; :: thesis: 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 f .: (Cl P) = Cl (f .: P) ) ) )
let f be Function of T,S; :: thesis: ( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds f .: (Cl P) = Cl (f .: P) ) ) )

hereby :: thesis: ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds f .: (Cl P) = Cl (f .: P) ) implies f is being_homeomorphism )

assume A1: f is being_homeomorphism ; :: thesis: ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds f .: (Cl P) = Cl (f .: P) ) )
then A2: ( f is continuous & f " is continuous ) by Def5;
thus A3: ( dom f = [#] T & rng f = [#] S & f is one-to-one ) by A1, Def5; :: thesis: for P being Subset of T holds f .: (Cl P) = Cl (f .: P)
let P be Subset of T; :: thesis: f .: (Cl P) = Cl (f .: P)
A4: f .: (Cl P) c= Cl (f .: P) by A2, Th57;
A5: Cl ((f " ) " P) c= (f " ) " (Cl P) by A2, Th56;
( (f " ) " P = f .: P & (f " ) " (Cl P) = f .: (Cl P) ) by A3, Th67;
hence f .: (Cl P) = Cl (f .: P) by A4, A5, XBOOLE_0:def 10; :: thesis: verum

end;

assume A6: ( dom f = [#] T & rng f = [#] S & f is one-to-one ) ; :: thesis: ( ex P being Subset of T st not f .: (Cl P) = Cl (f .: P) or f is being_homeomorphism )
assume A7: for P being Subset of T holds f .: (Cl P) = Cl (f .: P) ; :: thesis: f is being_homeomorphism
thus ( dom f = [#] T & rng f = [#] S & f is one-to-one ) by A6; :: according to TOPS_2:def 5 :: thesis: ( f is continuous & f " is continuous )
for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) by A7;
hence f is continuous by Th57; :: thesis: f " is continuous

now

let P be Subset of T; :: thesis: Cl ((f " ) " P) c= (f " ) " (Cl P)
( (f " ) " P = f .: P & (f " ) " (Cl P) = f .: (Cl P) ) by A6, Th67;
hence Cl ((f " ) " P) c= (f " ) " (Cl P) by A7; :: thesis: verum

end;

hence f " is continuous by Th56; :: thesis: verum