Upper_Arc S is_an_arc_of W-min S, E-max S by Def8;
hence ( not Upper_Arc S is empty & Upper_Arc S is compact ) by JORDAN5A:1; :: thesis: verum