let C be Simple_closed_curve; :: thesis: for q being Point of (TOP-REAL 2) st q in C holds
Segment q,(W-min C),C is compact
let q be Point of (TOP-REAL 2); :: thesis: ( q in C implies Segment q,(W-min C),C is compact )
assume A1: q in C ; :: thesis: Segment q,(W-min C),C is compact

per cases ( q = W-min C or q <> W-min C ) ;

suppose q = W-min C ; :: thesis: Segment q,(W-min C),C is compact

hence Segment q,(W-min C),C is compact by Th19; :: thesis: verum

end;

suppose q <> W-min C ; :: thesis: Segment q,(W-min C),C is compact

hence Segment q,(W-min C),C is compact by A1, Th17, JORDAN5A:1; :: thesis: verum

end;

end;