let P be non empty compact Subset of (TOP-REAL 2); 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); ( q1 in P & P is being_simple_closed_curve implies q1 in Segment (q1,(W-min P),P) )
assume A1:
q1 in P
; ( not P is being_simple_closed_curve or q1 in Segment (q1,(W-min P),P) )
assume
P is being_simple_closed_curve
; 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; verum