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 that
A1: P is being_simple_closed_curve and
A2: q1 <> W-min P and
A3: q2 <> W-min P ; :: thesis: not W-min P in Segment (q1,q2,P)
A4: Segment (q1,q2,P) = { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } by A3, Def1;

now :: thesis: not W-min P in Segment (q1,q2,P)

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

end;

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