let C be Simple_closed_curve; :: thesis: for i being Nat holds
( (Lower_Appr C) . i is compact & (Lower_Appr C) . i is connected )
let i be 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