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;

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 )
;

end;

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;then diameter (Segm (S,i)) in S1 by A1;

hence diameter (Segm (S,i)) <= diameter S by A2, XXREAL_2:def 8; :: thesis: verum

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;.= 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