:: deftheorem defines being_simple_closed_curve TOPREAL2:def 1 :
for P being Subset of (TOP-REAL 2) holds
( P is being_simple_closed_curve iff ex f being Function of ((TOP-REAL 2) | R^2-unit_square),((TOP-REAL 2) | P) st f is being_homeomorphism );