let C be Simple_closed_curve; :: thesis: for S being Segmentation of C
for i being Element of NAT holds diameter (Segm S,i) <= diameter S
let S be Segmentation of C; :: thesis: for i being Element of NAT holds diameter (Segm S,i) <= diameter S
let i be Element of NAT ; :: thesis: diameter (Segm S,i) <= diameter S
consider S1 being non empty finite Subset of REAL such that
A1: S1 = { (diameter (Segm S,j)) where j is Element of NAT : j in dom S } and
A2: diameter S = max S1 by Def6;

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

suppose ( 1 <= i & i < len S ) ; :: thesis: diameter (Segm S,i) <= diameter S

then i in dom S by FINSEQ_3:27;
then diameter (Segm S,i) in S1 by A1;
hence diameter (Segm S,i) <= diameter S by A2, XXREAL_2:def 8; :: thesis: verum

end;

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

A4: Segm S,(len S) = Segment (S /. (len S)),(S /. 1),C by Def4
.= Segm S,i by A3, Def4 ;
len S in dom S by FINSEQ_5:6;
then diameter (Segm S,i) in S1 by A1, A4;
hence diameter (Segm S,i) <= diameter S by A2, XXREAL_2:def 8; :: thesis: verum

end;

end;