let C be Simple_closed_curve; for e being Real st e > 0 holds
ex S being Segmentation of C st diameter S < e
let e be Real; ( e > 0 implies ex S being Segmentation of C st diameter S < e )
assume
e > 0
; 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
; diameter h < e
for i being Nat holds diameter (Segm (h,i)) < e
hence
diameter h < e
by Th33; verum