let x be Real; :: thesis: for A being closed-interval Subset of REAL
for D being Division of A st x in rng D holds
( D . 1 <= x & x <= D . (len D) )
let A be closed-interval Subset of REAL ; :: thesis: for D being Division of A st x in rng D holds
( D . 1 <= x & x <= D . (len D) )
let D be Division of A; :: thesis: ( x in rng D implies ( D . 1 <= x & x <= D . (len D) ) )
assume x in rng D ; :: thesis: ( D . 1 <= x & x <= D . (len D) )
then consider i being Element of NAT such that
A1: ( i in dom D & x = D . i ) by PARTFUN1:26;
A2: ( 1 <= i & i <= len D ) by A1, FINSEQ_3:27;
then 1 <= len D by XXREAL_0:2;
then ( 1 in dom D & len D in dom D ) by FINSEQ_3:27;
hence ( D . 1 <= x & x <= D . (len D) ) by A1, A2, GOBOARD2:18; :: thesis: verum