for P being non empty compact Subset of (TOP-REAL 2)
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)}