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 and
A2: x = D . i by PARTFUN1:26;
A3: i <= len D by A1, FINSEQ_3:27;
A4: 1 <= i by A1, FINSEQ_3:27;
then A5: 1 <= len D by A3, XXREAL_0:2;
then A6: len D in dom D by FINSEQ_3:27;
1 in dom D by A5, FINSEQ_3:27;
hence ( D . 1 <= x & x <= D . (len D) ) by A1, A2, A4, A3, A6, GOBOARD2:18; :: thesis: verum