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