let C be Simple_closed_curve; :: thesis: C is Jordan
consider f being Homeomorphism of TOP-REAL 2 such that
A1: |[(- 1),0]|,|[1,0]| realize-max-dist-in f .: C by JORDAN24:7;
A2: f " is Homeomorphism of TOP-REAL 2 by TOPGRP_1:30;
f .: C is Simple_closed_curve by Th70;
then f .: C is Jordan by A1, Lm91;
then A3: (f ") .: (f .: C) is Jordan by A2, JORDAN24:16;
A4: f " = f " by TOPS_2:def 4;
dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
hence C is Jordan by A3, A4, FUNCT_1:107; :: thesis: verum