let C be Simple_closed_curve; :: thesis: for S being Segmentation of C

for e being Real st ( for i being Nat holds diameter (Segm (S,i)) < e ) holds

diameter S < e

let S be Segmentation of C; :: thesis: for e being Real st ( for i being Nat holds diameter (Segm (S,i)) < e ) holds

diameter S < e

let e be Real; :: thesis: ( ( for i being Nat holds diameter (Segm (S,i)) < e ) implies diameter S < e )

assume A1: for i being Nat holds diameter (Segm (S,i)) < e ; :: thesis: diameter S < e

consider S1 being non empty finite Subset of REAL such that

A2: S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } and

A3: diameter S = max S1 by Def6;

diameter S in S1 by A3, XXREAL_2:def 8;

then ex i being Element of NAT st

( diameter S = diameter (Segm (S,i)) & i in dom S ) by A2;

hence diameter S < e by A1; :: thesis: verum

for e being Real st ( for i being Nat holds diameter (Segm (S,i)) < e ) holds

diameter S < e

let S be Segmentation of C; :: thesis: for e being Real st ( for i being Nat holds diameter (Segm (S,i)) < e ) holds

diameter S < e

let e be Real; :: thesis: ( ( for i being Nat holds diameter (Segm (S,i)) < e ) implies diameter S < e )

assume A1: for i being Nat holds diameter (Segm (S,i)) < e ; :: thesis: diameter S < e

consider S1 being non empty finite Subset of REAL such that

A2: S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } and

A3: diameter S = max S1 by Def6;

diameter S in S1 by A3, XXREAL_2:def 8;

then ex i being Element of NAT st

( diameter S = diameter (Segm (S,i)) & i in dom S ) by A2;

hence diameter S < e by A1; :: thesis: verum