let C be Simple_closed_curve; :: thesis: for S being Segmentation of C
for i being Nat holds diameter (Segm (S,i)) <= diameter S
let S be Segmentation of C; :: thesis: for i being Nat holds diameter (Segm (S,i)) <= diameter S
let i be 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:25;
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;