let A be non empty closed_interval Subset of REAL; :: thesis: A = [.(lower_bound A),(upper_bound A).]
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: ( 0 < y implies ex x being Real st
( x in A & b - y < x ) )
assume A4: 0 < y ; :: thesis: ex x being Real st
( x in A & b - y < x )
take b ; :: thesis: ( b in A & b - y < b )
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: verum

end;

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

proof

let x be Real; :: thesis: ( x in A implies x <= b )
assume A6: x in A ; :: thesis: x <= b
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: verum

end;

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

proof

let x be Real; :: thesis: ( x in A implies a <= x )
assume A8: x in A ; :: thesis: a <= x
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: verum

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: ( 0 < y implies ex x being Real st
( x in A & x < a + y ) )
assume A9: 0 < y ; :: thesis: ex x being Real st
( x in A & x < a + y )
take a ; :: thesis: ( a in A & a < a + y )
thus ( a in A & a < a + y ) by A1, A2, A9, XREAL_1:29, XXREAL_1:1; :: thesis: verum

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: verum