let A be non empty closed_interval Subset of REAL; :: thesis:
consider a, b being Real such that
A1: a <= b and
A2: A = [.a,b.] by MEASURE5:14;
A3: for y being Real st 0 < y holds
ex x being Real st
( x in A & b - y < x )

proof

let y be Real; :: thesis:
assume A4: 0 < y ; :: thesis:
take b ; :: thesis:
b < b + y by A4, XREAL_1:29;
then b - y < (b + y) - y by XREAL_1:9;
hence ( b in A & b - y < b ) by A1, A2, XXREAL_1:1; :: thesis:

end;

A5: for x being Real st x in A holds
x <= b

proof

let x be Real; :: thesis:
assume A6: x in A ; :: thesis:
A = { y where y is Real : ( a <= y & y <= b ) } by A2, RCOMP_1:def 1;
then ex y being Real st
( x = y & a <= y & y <= b ) by A6;
hence x <= b ; :: thesis:

end;

A7: for x being Real st x in A holds
a <= x

proof

let x be Real; :: thesis:
assume A8: x in A ; :: thesis:
A = { y where y is Real : ( a <= y & y <= b ) } by A2, RCOMP_1:def 1;
then ex y being Real st
( x = y & a <= y & y <= b ) by A8;
hence a <= x ; :: thesis:

end;

for y being Real st 0 < y holds
ex x being Real st
( x in A & x < a + y )

proof

let y be Real; :: thesis:
assume A9: 0 < y ; :: thesis:
take a ; :: thesis:
thus ( a in A & a < a + y ) by A1, A2, A9, XREAL_1:29, XXREAL_1:1; :: thesis:

end;

then a = lower_bound A by A7, SEQ_4:def 2;
hence A = [.(lower_bound A),(upper_bound A).] by A2, A5, A3, SEQ_4:def 1; :: thesis: