let D be Simple_closed_curve; :: thesis: (TOP-REAL 2) | R^2-unit_square,(TOP-REAL 2) | D are_homeomorphic
ex f being Function of ((TOP-REAL 2) | R^2-unit_square),((TOP-REAL 2) | D) st f is being_homeomorphism by TOPREAL2:def 1;
hence (TOP-REAL 2) | R^2-unit_square,(TOP-REAL 2) | D are_homeomorphic by T_0TOPSP:def 1; :: thesis: verum