let T be non empty TopSpace; :: thesis: for S being 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 P1 being Subset of S holds f " (Cl P1) = Cl (f " P1) ) ) )
let S be 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 P1 being Subset of S holds f " (Cl P1) = Cl (f " P1) ) ) )
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 P1 being Subset of S holds f " (Cl P1) = Cl (f " P1) ) ) )

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

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

end;

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

now :: thesis: for P1 being Subset of S holds (f ") .: (Cl P1) c= Cl ((f ") .: P1)

let P1 be Subset of S; :: thesis: (f ") .: (Cl P1) c= Cl ((f ") .: P1)
( (f ") .: (Cl P1) = f " (Cl P1) & (f ") .: P1 = f " P1 ) by A6, Th55;
hence (f ") .: (Cl P1) c= Cl ((f ") .: P1) by A7; :: thesis: verum

end;

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