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

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:55; :: 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:147; :: thesis:

end;

assume that
A5: ( dom f = [#] S & rng f = [#] T & f is one-to-one ) and
A6: for P being Subset of T holds
( P is open iff f " P is open ) ; :: thesis:
thus ( dom f = [#] S & rng f = [#] T & f is one-to-one ) by A5; :: according to TOPS_2:def 5 :: thesis:
thus f is continuous by A1, A6, TOPS_2:55; :: thesis:

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

end;

hence f /" is continuous by A1, TOPS_2:55; :: thesis: