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

end;

end;