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