let C be Simple_closed_curve; :: thesis:
let S be Segmentation of C; :: thesis:
let i be Nat; :: thesis:
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 ;

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

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:

end;

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

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:

end;

end;