let S, T be being_simple_closed_curve SubSpace of TOP-REAL 2; S,T are_homeomorphic
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
((TOP-REAL 2) | R^2-unit_square),
((TOP-REAL 2) | A) such that A1:
f is
being_homeomorphism
by TOPREAL2:def 1;
A2:
f " is
being_homeomorphism
by A1, TOPS_2:56;
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 #)
= (TOP-REAL 2) | A
by A3, PRE_TOPC:def 5;
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
((TOP-REAL 2) | R^2-unit_square),
((TOP-REAL 2) | 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 A4, A6, PRE_TOPC:def 5;
take
h
;
T_0TOPSP:def 1 h is being_homeomorphism
TopStruct(# the
carrier of
T, the
topology of
T #)
= (TOP-REAL 2) | B
by A7, A6, PRE_TOPC:def 5;
hence
h is
being_homeomorphism
by A5, A4, A2, TOPS_2:57;
verum
end;
hence
S,T are_homeomorphic
by TOPREALA:15; verum