let S be TopSpace; :: thesis: for T being non empty TopSpace holds
( S,T are_homeomorphic iff TopStruct(# the carrier of S,the topology of S #), TopStruct(# the carrier of T,the topology of T #) are_homeomorphic )
let T be non empty TopSpace; :: thesis: ( S,T are_homeomorphic iff TopStruct(# the carrier of S,the topology of S #), TopStruct(# the carrier of T,the topology of T #) are_homeomorphic )
set SS = TopStruct(# the carrier of S,the topology of S #);
set TT = TopStruct(# the carrier of T,the topology of T #);
A1: [#] S = [#] TopStruct(# the carrier of S,the topology of S #) ;
A2: [#] T = [#] TopStruct(# the carrier of T,the topology of T #) ;
thus ( S,T are_homeomorphic implies TopStruct(# the carrier of S,the topology of S #), TopStruct(# the carrier of T,the topology of T #) are_homeomorphic ) :: thesis: ( TopStruct(# the carrier of S,the topology of S #), TopStruct(# the carrier of T,the topology of T #) are_homeomorphic implies S,T are_homeomorphic )

proof

given f being Function of S,T such that A3: f is being_homeomorphism ; :: according to T_0TOPSP:def 1 :: thesis: TopStruct(# the carrier of S,the topology of S #), TopStruct(# the carrier of T,the topology of T #) are_homeomorphic
reconsider g = f as Function of TopStruct(# the carrier of S,the topology of S #),TopStruct(# the carrier of T,the topology of T #) ;
take g ; :: according to T_0TOPSP:def 1 :: thesis: g is being_homeomorphism
A4: ( dom f = [#] S & rng f = [#] T & f is one-to-one ) by A3, TOPS_2:74;

now

let P be Subset of TopStruct(# the carrier of S,the topology of S #); :: thesis: g .: (Cl P) = Cl (g .: P)
reconsider R = P as Subset of S ;
thus g .: (Cl P) = f .: (Cl R) by TOPS_3:80
.= Cl (f .: R) by A3, TOPS_2:74
.= Cl (g .: P) by TOPS_3:80 ; :: thesis: verum

end;

hence g is being_homeomorphism by A1, A2, A4, TOPS_2:74; :: thesis: verum

end;

given f being Function of TopStruct(# the carrier of S,the topology of S #),TopStruct(# the carrier of T,the topology of T #) such that A5: f is being_homeomorphism ; :: according to T_0TOPSP:def 1 :: thesis: S,T are_homeomorphic
reconsider g = f as Function of S,T ;
take g ; :: according to T_0TOPSP:def 1 :: thesis: g is being_homeomorphism
A6: ( dom f = [#] TopStruct(# the carrier of S,the topology of S #) & rng f = [#] TopStruct(# the carrier of T,the topology of T #) & f is one-to-one ) by A5, TOPS_2:74;

now

let P be Subset of S; :: thesis: g .: (Cl P) = Cl (g .: P)
reconsider R = P as Subset of TopStruct(# the carrier of S,the topology of S #) ;
thus g .: (Cl P) = f .: (Cl R) by TOPS_3:80
.= Cl (f .: R) by A5, TOPS_2:74
.= Cl (g .: P) by TOPS_3:80 ; :: thesis: verum

end;

hence g is being_homeomorphism by A1, A2, A6, TOPS_2:74; :: thesis: verum