let x be Real; :: thesis: for A being non empty 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 non empty 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 and
A2: x = D . i by PARTFUN1:3;
A3: i <= len D by A1, FINSEQ_3:25;
A4: 1 <= i by A1, FINSEQ_3:25;
then A5: 1 <= len D by A3, XXREAL_0:2;
then A6: len D in dom D by FINSEQ_3:25;
1 in dom D by A5, FINSEQ_3:25;
hence ( D . 1 <= x & x <= D . (len D) ) by A1, A2, A4, A3, A6, SEQ_4:137; :: thesis: verum