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