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 that
A1: P is being_simple_closed_curve and
A2: q in P ; :: thesis: LE W-min P,q,P
A3: q in (Upper_Arc P) \/ (Lower_Arc P) by A1, A2, JORDAN6:50;
A4: Upper_Arc P is_an_arc_of W-min P, E-max P by A1, JORDAN6:50;
A5: W-min P in Upper_Arc P by A1, Th1;

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

suppose A6: 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 A4, JORDAN5C:10;
hence LE W-min P,q,P by A5, A6, JORDAN6:def 10; :: thesis: verum

end;

suppose A7: 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 A5, A7, JORDAN6:def 10; :: thesis: verum

end;

suppose A8: 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 A5, JORDAN5C:9;
hence LE W-min P,q,P by A5, A8, JORDAN6:def 10; :: thesis: verum

end;

end;

end;

end;