for C being Simple_closed_curve
for q1, q2 being Point of (TOP-REAL 2) st LE q1,q2,C holds
Segment (q1,q2,C) is compact