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 & LE q1,q2,P & q1 <> q2 & q1 <> W-min P holds
(Segment q2,(W-min P),P) /\ (Segment (W-min P),q1,P) = {(W-min P)}
let q1, q2 be Point of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve & LE q1,q2,P & q1 <> q2 & q1 <> W-min P implies (Segment q2,(W-min P),P) /\ (Segment (W-min P),q1,P) = {(W-min P)} )
assume A1: ( P is being_simple_closed_curve & LE q1,q2,P & q1 <> q2 & q1 <> W-min P ) ; :: thesis: (Segment q2,(W-min P),P) /\ (Segment (W-min P),q1,P) = {(W-min P)}
then A2: ( q1 in P & q2 in P ) by Th5;
thus (Segment q2,(W-min P),P) /\ (Segment (W-min P),q1,P) c= {(W-min P)} :: according to XBOOLE_0:def 10 :: thesis: {(W-min P)} c= (Segment q2,(W-min P),P) /\ (Segment (W-min P),q1,P)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (Segment q2,(W-min P),P) /\ (Segment (W-min P),q1,P) or x in {(W-min P)} )
assume x in (Segment q2,(W-min P),P) /\ (Segment (W-min P),q1,P) ; :: thesis: x in {(W-min P)}
then A3: ( x in Segment q2,(W-min P),P & x in Segment (W-min P),q1,P ) by XBOOLE_0:def 4;
then x in { p1 where p1 is Point of (TOP-REAL 2) : ( LE q2,p1,P or ( q2 in P & p1 = W-min P ) ) } by Def1;
then consider p1 being Point of (TOP-REAL 2) such that
A4: ( p1 = x & ( LE q2,p1,P or ( q2 in P & p1 = W-min P ) ) ) ;

now

per cases ( LE q2,p1,P or ( q2 in P & p1 = W-min P ) ) by A4;

case A5: LE q2,p1,P ; :: thesis: contradiction

x in { p where p is Point of (TOP-REAL 2) : ( LE W-min P,p,P & LE p,q1,P ) } by A1, A3, Def1;
then ex p2 being Point of (TOP-REAL 2) st
( p2 = x & LE W-min P,p2,P & LE p2,q1,P ) ;
then LE q2,q1,P by A1, A4, A5, JORDAN6:73;
hence contradiction by A1, JORDAN6:72; :: thesis: verum

end;

case ( q2 in P & p1 = W-min P ) ; :: thesis: x = W-min P

hence x = W-min P by A4; :: thesis: verum

end;

end;

end;

hence x in {(W-min P)} by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(W-min P)} or x in (Segment q2,(W-min P),P) /\ (Segment (W-min P),q1,P) )
assume x in {(W-min P)} ; :: thesis: x in (Segment q2,(W-min P),P) /\ (Segment (W-min P),q1,P)
then A6: x = W-min P by TARSKI:def 1;
then x in { p1 where p1 is Point of (TOP-REAL 2) : ( LE q2,p1,P or ( q2 in P & p1 = W-min P ) ) } by A2;
then A7: x in Segment q2,(W-min P),P by Def1;
LE W-min P,q1,P by A1, A2, Th3;
then x in Segment (W-min P),q1,P by A1, A6, Th6;
hence x in (Segment q2,(W-min P),P) /\ (Segment (W-min P),q1,P) by A7, XBOOLE_0:def 4; :: thesis: verum