let C be being_simple_closed_curve Subset of (TOP-REAL 2); :: thesis: ApproxIndex C >= 1
ApproxIndex C is_sufficiently_large_for C by Def1;
hence ApproxIndex C >= 1 by JORDAN1H:51; :: thesis: verum