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 Nat st 1 <= i & i < len h holds
LE h /. i,h /. (i + 1),C and
A6: for i being 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 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 Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds
Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) and
A13: for i being 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:20;
h <> {} by A3, CARD_1:27;
then 1 in dom h by FINSEQ_5:6;
then h /. 1 = W-min C by A1, PARTFUN1:def 6;
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 Nat holds diameter (Segm (h,i)) < e
proof
let i be 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 Th33; :: thesis: verum