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 ) by TOPS_2:def 5; :: thesis:
let P be Subset of T; :: thesis:

hereby :: thesis:

assume A4: P is open ; :: thesis:
f is continuous by A2, TOPS_2:def 5;
hence f " P is open by A1, A4, TOPS_2:43; :: thesis:

end;

assume f " P is open ; :: thesis:
then f .: (f " P) is open by A2, Th25;
hence P is open by A3, FUNCT_1:77; :: thesis:

end;

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

A9: now

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

end;

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