let C be Simple_closed_curve; :: thesis: for i being Element of NAT holds
( (Lower_Appr C) . i is compact & (Lower_Appr C) . i is connected )
let i be Element of NAT ; :: thesis: ( (Lower_Appr C) . i is compact & (Lower_Appr C) . i is connected )
Lower_Arc (L~ (Cage C,i)) is compact ;
hence (Lower_Appr C) . i is compact by JORDAN19:def 2; :: thesis: (Lower_Appr C) . i is connected
Lower_Arc (L~ (Cage C,i)) is connected ;
hence (Lower_Appr C) . i is connected by JORDAN19:def 2; :: thesis: verum