for P, Q being Subset of (TOP-REAL 2) st ex f being Function of ((TOP-REAL 2) | P),((TOP-REAL 2) | Q) st f is being_homeomorphism & P is being_simple_closed_curve holds
Q is being_simple_closed_curve