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:61;
A2: L~ (Cage (C,i)) c= Cl (RightComp (Cage (C,0))) by JORDAN1H:46;
(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