let C be Simple_closed_curve; :: thesis: for i being Element of NAT holds (Upper_Appr C) . i c= Cl (RightComp (Cage C,0 ))
let i be Element of NAT ; :: thesis: (Upper_Appr C) . i c= Cl (RightComp (Cage C,0 ))
A1: (Upper_Appr C) . i = Upper_Arc (L~ (Cage C,i)) by JORDAN19:def 1;
A2: Upper_Arc (L~ (Cage C,i)) c= L~ (Cage C,i) by JORDAN6:76;
L~ (Cage C,i) c= Cl (RightComp (Cage C,0 )) by JORDAN1H:54;
hence (Upper_Appr C) . i c= Cl (RightComp (Cage C,0 )) by A1, A2, XBOOLE_1:1; :: thesis: verum