let P be non empty compact Subset of (TOP-REAL 2); :: thesis: for q1, q2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & q1 <> W-min P & q2 <> W-min P holds
not W-min P in Segment q1,q2,P
let q1, q2 be Point of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve & q1 <> W-min P & q2 <> W-min P implies not W-min P in Segment q1,q2,P )
assume A1: ( P is being_simple_closed_curve & q1 <> W-min P & q2 <> W-min P ) ; :: thesis: not W-min P in Segment q1,q2,P
then A2: Segment q1,q2,P = { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } by Def1;

now

assume W-min P in Segment q1,q2,P ; :: thesis: contradiction
then consider p being Point of (TOP-REAL 2) such that
A3: ( p = W-min P & LE q1,p,P & LE p,q2,P ) by A2;
A4: ( q1 in Upper_Arc P & p in Upper_Arc P & LE q1,p, Upper_Arc P, W-min P, E-max P ) by A3, JORDAN6:def 10;
Upper_Arc P is_an_arc_of W-min P, E-max P by A1, JORDAN6:def 8;
hence contradiction by A1, A3, A4, JORDAN6:69; :: thesis: verum

end;

hence not W-min P in Segment q1,q2,P ; :: thesis: verum