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

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