let C be Simple_closed_curve; :: thesis: for e being Real st e > 0 holds
ex S being Segmentation of C st diameter S < e
let e be Real; :: thesis: ( e > 0 implies ex S being Segmentation of C st diameter S < e )
assume e > 0 ; :: thesis: ex S being Segmentation of C st diameter S < e
then consider h being FinSequence of the carrier of (TOP-REAL 2) such that
A1: h . 1 = W-min C and
A2: h is one-to-one and
A3: 8 <= len h and
A4: rng h c= C and
A5: for i being Element of NAT st 1 <= i & i < len h holds
LE h /. i,h /. (i + 1),C and
A6: for i being Element of NAT
for W being Subset of (Euclid 2) st 1 <= i & i < len h & W = Segment (h /. i),(h /. (i + 1)),C holds
diameter W < e and
A7: for W being Subset of (Euclid 2) st W = Segment (h /. (len h)),(h /. 1),C holds
diameter W < e and
A8: for i being Element of NAT st 1 <= i & i + 1 < len h holds
(Segment (h /. i),(h /. (i + 1)),C) /\ (Segment (h /. (i + 1)),(h /. (i + 2)),C) = {(h /. (i + 1))} and
A9: (Segment (h /. (len h)),(h /. 1),C) /\ (Segment (h /. 1),(h /. 2),C) = {(h /. 1)} and
A10: (Segment (h /. ((len h) -' 1)),(h /. (len h)),C) /\ (Segment (h /. (len h)),(h /. 1),C) = {(h /. (len h))} and
A11: Segment (h /. ((len h) -' 1)),(h /. (len h)),C misses Segment (h /. 1),(h /. 2),C and
A12: for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment (h /. i),(h /. (i + 1)),C misses Segment (h /. j),(h /. (j + 1)),C and
A13: for i being Element of NAT st 1 < i & i + 1 < len h holds
Segment (h /. (len h)),(h /. 1),C misses Segment (h /. i),(h /. (i + 1)),C by JORDAN7:21;
h <> {} by A3, CARD_1:47;
then 1 in dom h by FINSEQ_5:6;
then h /. 1 = W-min C by A1, PARTFUN1:def 8;
then reconsider h = h as Segmentation of C by A2, A3, A4, A5, A8, A9, A10, A11, A12, A13, Def3;
take h ; :: thesis: diameter h < e
for i being Element of NAT holds diameter (Segm h,i) < e

proof

let i be Element of NAT ; :: thesis: diameter (Segm h,i) < e
A14: ex W being Subset of (Euclid 2) st
( W = Segm h,i & diameter (Segm h,i) = diameter W ) by Def5;

per cases ( ( 1 <= i & i < len h ) or not 1 <= i or not i < len h ) ;

suppose A15: ( 1 <= i & i < len h ) ; :: thesis: diameter (Segm h,i) < e

then Segm h,i = Segment (h /. i),(h /. (i + 1)),C by Def4;
hence diameter (Segm h,i) < e by A6, A14, A15; :: thesis: verum

end;

suppose ( not 1 <= i or not i < len h ) ; :: thesis: diameter (Segm h,i) < e

then Segm h,i = Segment (h /. (len h)),(h /. 1),C by Def4;
hence diameter (Segm h,i) < e by A7, A14; :: thesis: verum

end;

end;

end;

hence diameter h < e by Th34; :: thesis: verum