:: deftheorem defines North_Arc JORDAN19:def 3 :
for C being Simple_closed_curve holds North_Arc C = Lim_inf (Upper_Appr C);