let C be Simple_closed_curve; :: thesis: for i being Nat holds (Upper_Appr C) . i c= Cl (RightComp (Cage (C,0)))
let i be Nat; :: thesis: (Upper_Appr C) . i c= Cl (RightComp (Cage (C,0)))
A1: Upper_Arc (L~ (Cage (C,i))) c= L~ (Cage (C,i)) by JORDAN6:61;
A2: L~ (Cage (C,i)) c= Cl (RightComp (Cage (C,0))) by JORDAN1H:46;
(Upper_Appr C) . i = Upper_Arc (L~ (Cage (C,i))) by JORDAN19:def 1;
hence (Upper_Appr C) . i c= Cl (RightComp (Cage (C,0))) by A1, A2; :: thesis: verum