for i being Nat holds (Lower_Appr C) . i c= Cl (RightComp (Cage (C,0))) by Th2;
then Lim_inf (Lower_Appr C) is compact by KURATO_2:26;
hence South_Arc C is compact by JORDAN19:def 4; :: thesis: verum