for i being Nat holds (Upper_Appr C) . i c= Cl (RightComp (Cage (C,0))) by Th1;
then Lim_inf (Upper_Appr C) is compact by KURATO_2:26;
hence North_Arc C is compact by JORDAN19:def 3; :: thesis: verum