let S, T be being_simple_closed_curve SubSpace of TOP-REAL 2; :: thesis: S,T are_homeomorphic

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

proof

hence
S,T are_homeomorphic
by TOPREALA:15; :: thesis: verum
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 ; :: according to T_0TOPSP:def 1 :: thesis: 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; :: thesis: verum

end;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 ; :: according to T_0TOPSP:def 1 :: thesis: 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; :: thesis: verum