let C be Simple_closed_curve; :: thesis:
let q1, q2 be Point of (TOP-REAL 2); :: thesis:
assume A1: LE q1,q2,C ; :: thesis:
A2: q1 in C by A1, JORDAN7:5;

suppose q2 = W-min C ; :: thesis:

hence Segment (q1,q2,C) is compact by A2, Th19; :: thesis:

end;

suppose ( q1 = q2 & q2 <> W-min C ) ; :: thesis:

then Segment (q1,q2,C) = {q1} by A2, JORDAN7:8;
hence Segment (q1,q2,C) is compact ; :: thesis:

end;

suppose ( q1 <> q2 & q2 <> W-min C ) ; :: thesis:

hence Segment (q1,q2,C) is compact by A1, Th17, JORDAN5A:1; :: thesis:

end;

end;