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 A1: ( P is being_simple_closed_curve & LE q, W-min P,P ) ; :: thesis: q = W-min P
then A2: ( q in Upper_Arc P & W-min P in Upper_Arc P & LE q, W-min P, Upper_Arc P, W-min P, E-max P ) by JORDAN6:def 10;
Upper_Arc P is_an_arc_of W-min P, E-max P by A1, JORDAN6:def 8;
hence q = W-min P by A2, JORDAN6:69; :: thesis: verum