theorem Th18: :: JORDAN_A:18

for C being Simple_closed_curve holds C = Segment ((W-min C),(W-min C),C)