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 ; :: 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 ;
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 ; :: thesis: verum
end;
end;