let S, T be non empty TopStruct ; :: thesis:
let f be Function of S,T; :: thesis:
A1: [#] T <> {} ;

hereby :: thesis:

assume A2: f is being_homeomorphism ; :: thesis:
hence A3: ( dom f = [#] S & rng f = [#] T & f is one-to-one ) ; :: thesis:
let P be Subset of T; :: thesis:
thus ( P is open implies f " P is open ) by A2, TOPS_2:43; :: thesis:
assume f " P is open ; :: thesis:
then f .: (f " P) is open by A2, Th24;
hence P is open by A3, FUNCT_1:77; :: thesis:

end;

assume that
A4: dom f = [#] S and
A5: rng f = [#] T and
A6: f is one-to-one and
A7: for P being Subset of T holds
( P is open iff f " P is open ) ; :: thesis:

A8: now :: thesis:

let R be Subset of S; :: thesis:
assume A9: R is open ; :: thesis:
for x1, x2 being Element of S st x1 in R & f . x1 = f . x2 holds
x2 in R by A4, A6;
then A10: f " (f .: R) = R by T_0TOPSP:1;
(f /") " R = f .: R by A5, A6, TOPS_2:54;
hence (f /") " R is open by A7, A9, A10; :: thesis:

end;

thus ( dom f = [#] S & rng f = [#] T & f is one-to-one ) by A4, A5, A6; :: according to TOPS_2:def 5 :: thesis:
thus f is continuous by A1, A7, TOPS_2:43; :: thesis:
[#] S <> {} ;
hence f /" is continuous by A8, TOPS_2:43; :: thesis: