let P be non empty compact Subset of (TOP-REAL 2); :: thesis: for q being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q, W-min P,P holds

q = W-min P

let q be Point of (TOP-REAL 2); :: 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:54; :: thesis: verum

q = W-min P

let q be Point of (TOP-REAL 2); :: 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:54; :: thesis: verum