let C be Simple_closed_curve; :: thesis: for q1, q2 being Point of (TOP-REAL 2) st LE q1,q2,C holds
Segment (q1,q2,C) is compact
let q1, q2 be Point of (TOP-REAL 2); :: thesis: ( LE q1,q2,C implies Segment (q1,q2,C) is compact )
assume A1: LE q1,q2,C ; :: thesis: Segment (q1,q2,C) is compact
A2: q1 in C by A1, JORDAN7:5;

per cases ( q2 = W-min C or ( q1 = q2 & q2 <> W-min C ) or ( q1 <> q2 & q2 <> W-min C ) ) ;

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

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

end;

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

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

end;

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

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

end;

end;