let S be TopSpace; 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; ( 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 )
( 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
;
T_0TOPSP:def 1 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
;
T_0TOPSP:def 1 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;
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
; T_0TOPSP:def 1 S,T are_homeomorphic
reconsider g = f as Function of S,T ;
take
g
; T_0TOPSP:def 1 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; verum