let P be non empty compact Subset of (TOP-REAL 2); :: thesis: for q1 being Point of (TOP-REAL 2) st q1 in P & P is being_simple_closed_curve holds
q1 in Segment q1,(W-min P),P
let q1 be Point of (TOP-REAL 2); :: thesis: ( q1 in P & P is being_simple_closed_curve implies q1 in Segment q1,(W-min P),P )
assume A1: q1 in P ; :: thesis: ( not P is being_simple_closed_curve or q1 in Segment q1,(W-min P),P )
assume P is being_simple_closed_curve ; :: thesis: q1 in Segment q1,(W-min P),P
then LE q1,q1,P by A1, JORDAN6:71;
then q1 in { p1 where p1 is Point of (TOP-REAL 2) : ( LE q1,p1,P or ( q1 in P & p1 = W-min P ) ) } ;
hence q1 in Segment q1,(W-min P),P by Def1; :: thesis: verum