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 #) & [#] 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 A2: 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 #) ;
A3: now :: thesis: for P being Subset of TopStruct(# the carrier of S, the topology of S #) holds g .: (Cl P) = Cl (g .: P)
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 A2, TOPS_2:60
.= Cl (g .: P) by TOPS_3:80 ; :: thesis: verum
end;
take g ; :: according to T_0TOPSP:def 1 :: thesis: g is being_homeomorphism
( dom f = [#] S & rng f = [#] T ) by A2, TOPS_2:60;
hence g is being_homeomorphism by A1, A2, A3, TOPS_2:60; :: 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 A4: f is being_homeomorphism ; :: according to T_0TOPSP:def 1 :: thesis: S,T are_homeomorphic
reconsider g = f as Function of S,T ;
A5: now :: thesis: for P being Subset of S holds g .: (Cl P) = Cl (g .: P)
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 A4, TOPS_2:60
.= Cl (g .: P) by TOPS_3:80 ; :: thesis: verum
end;
take g ; :: according to T_0TOPSP:def 1 :: thesis: g is being_homeomorphism
( dom f = [#] TopStruct(# the carrier of S, the topology of S #) & rng f = [#] TopStruct(# the carrier of T, the topology of T #) ) by A4, TOPS_2:60;
hence g is being_homeomorphism by A1, A4, A5, TOPS_2:60; :: thesis: verum