let P be non empty compact Subset of ; :: thesis: for q being Point of st P is being_simple_closed_curve & LE q, W-min P,P holds
q = W-min P
let q be Point of ; :: thesis: ( P is being_simple_closed_curve & LE q, W-min P,P implies q = W-min P )
assume ( P is being_simple_closed_curve & LE q, W-min P,P ) ; :: thesis: q = W-min P
then ( LE q, W-min P, Upper_Arc P, W-min P, E-max P & Upper_Arc P is_an_arc_of W-min P, E-max P ) by JORDAN6:def 8, JORDAN6:def 10;
hence q = W-min P by JORDAN6:69; :: thesis: verum