Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:def 9;
hence Lower_Arc C is connected by JORDAN6:10; :: thesis: verum