let S, T be being_simple_closed_curve SubSpace of TOP-REAL 2; :: thesis:
TopStruct(# the carrier of S, the topology of S #), TopStruct(# the carrier of T, the topology of T #) are_homeomorphic
proof
reconsider A = the carrier of TopStruct(# the carrier of S, the topology of S #) as Simple_closed_curve by Def5;
consider f being Function of (),(() | A) such that
A1: f is being_homeomorphism by TOPREAL2:def 1;
A2: f " is being_homeomorphism by ;
A3: [#] TopStruct(# the carrier of S, the topology of S #) = A ;
TopStruct(# the carrier of S, the topology of S #) is strict SubSpace of TOP-REAL 2 by TMAP_1:6;
then A4: TopStruct(# the carrier of S, the topology of S #) = () | A by ;
reconsider B = the carrier of TopStruct(# the carrier of T, the topology of T #) as Simple_closed_curve by Def5;
consider g being Function of (),(() | B) such that
A5: g is being_homeomorphism by TOPREAL2:def 1;
A6: [#] TopStruct(# the carrier of T, the topology of T #) = B ;
A7: TopStruct(# the carrier of T, the topology of T #) is strict SubSpace of TOP-REAL 2 by TMAP_1:6;
then reconsider h = g * (f ") as Function of TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #) by ;
take h ; :: according to T_0TOPSP:def 1 :: thesis:
TopStruct(# the carrier of T, the topology of T #) = () | B by ;
hence h is being_homeomorphism by ; :: thesis: verum
end;
hence S,T are_homeomorphic by TOPREALA:15; :: thesis: verum