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 & q in P holds
LE W-min P,q,P
let q be Point of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve & q in P implies LE W-min P,q,P )
assume A1: ( P is being_simple_closed_curve & q in P ) ; :: thesis: LE W-min P,q,P
then A2: q in (Upper_Arc P) \/ (Lower_Arc P) by JORDAN6:65;
A3: ( Upper_Arc P is_an_arc_of W-min P, E-max P & Lower_Arc P is_an_arc_of E-max P, W-min P ) by A1, JORDAN6:65;
A4: W-min P in Upper_Arc P by A1, Th1;

per cases ( q in Upper_Arc P or q in Lower_Arc P ) by A2, XBOOLE_0:def 3;

suppose A5: q in Upper_Arc P ; :: thesis: LE W-min P,q,P

then LE W-min P,q, Upper_Arc P, W-min P, E-max P by A3, JORDAN5C:10;
hence LE W-min P,q,P by A4, A5, JORDAN6:def 10; :: thesis: verum

end;

suppose A6: q in Lower_Arc P ; :: thesis: LE W-min P,q,P

per cases ( not q = W-min P or q = W-min P ) ;

suppose not q = W-min P ; :: thesis: LE W-min P,q,P

hence LE W-min P,q,P by A4, A6, JORDAN6:def 10; :: thesis: verum

end;

suppose A7: q = W-min P ; :: thesis: LE W-min P,q,P

then LE W-min P,q, Upper_Arc P, W-min P, E-max P by A4, JORDAN5C:9;
hence LE W-min P,q,P by A4, A7, JORDAN6:def 10; :: thesis: verum

end;

end;

end;

end;