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 Th18; :: 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, Th16, JORDAN5A:1; :: thesis: verum

end;

end;