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