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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (Segment q1,q2,P) /\ (Segment q2,(W-min P),P) or x in {q2} )
assume x in (Segment q1,q2,P) /\ (Segment q2,(W-min P),P) ; :: thesis: x in {q2}
then A2: ( x in Segment q1,q2,P & x in Segment q2,(W-min P),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
A3: p1 = x and
A4: ( LE q2,p1,P or ( q2 in P & p1 = W-min P ) ) ;
p1 in { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } by A1, A2, A3, Def1;
then A5: ex p being Point of (TOP-REAL 2) st
( p = p1 & LE q1,p,P & LE p,q2,P ) ;

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

suppose LE q2,p1,P ; :: thesis: x in {q2}

then x = q2 by A1, A3, A5, JORDAN6:72;
hence x in {q2} by TARSKI:def 1; :: thesis: verum

end;

suppose ( q2 in P & p1 = W-min P ) ; :: thesis: x in {q2}

hence x in {q2} by A1, A5, Th2; :: thesis: verum

end;

end;

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {q2} or x in (Segment q1,q2,P) /\ (Segment q2,(W-min P),P) )
assume x in {q2} ; :: thesis: x in (Segment q1,q2,P) /\ (Segment q2,(W-min P),P)
then A6: x = q2 by TARSKI:def 1;
then A7: x in Segment q1,q2,P by A1, Th6;
q2 in P by A1, Th5;
then x in Segment q2,(W-min P),P by A1, A6, Th7;
hence x in (Segment q1,q2,P) /\ (Segment q2,(W-min P),P) by A7, XBOOLE_0:def 4; :: thesis: verum