for C being Simple_closed_curve
for i being Nat holds (Upper_Appr C) . i c= Cl (RightComp (Cage (C,0)))