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