:: deftheorem defines South_Arc JORDAN19:def 4 :
for C being Simple_closed_curve holds South_Arc C = Lim_inf (Lower_Appr C);