let C be Simple_closed_curve; :: thesis: for i being Nat holds
( (Upper_Appr C) . i is compact & (Upper_Appr C) . i is connected )
let i be Nat; :: thesis: ( (Upper_Appr C) . i is compact & (Upper_Appr C) . i is connected )
Upper_Arc (L~ (Cage (C,i))) is compact ;
hence (Upper_Appr C) . i is compact by JORDAN19:def 1; :: thesis: (Upper_Appr C) . i is connected
Upper_Arc (L~ (Cage (C,i))) is connected ;
hence (Upper_Appr C) . i is connected by JORDAN19:def 1; :: thesis: verum