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:56;

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

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:56;

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