let A be 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 Def1;
A3: for y being real number st 0 < y holds
ex x being real number st
( x in A & b - y < x )

proof

let y be real number ; :: thesis: ( 0 < y implies ex x being real number st
( x in A & b - y < x ) )
assume A4: 0 < y ; :: thesis: ex x being real number st
( x in A & b - y < x )
take b ; :: thesis: ( b in A & b - y < b )
b < b + y by A4, XREAL_1:31;
then b - y < (b + y) - y by XREAL_1:11;
hence ( b in A & b - y < b ) by A1, A2, XXREAL_1:1; :: thesis: verum

end;

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

proof

let x be real number ; :: 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 number st x in A holds
a <= x

proof

let x be real number ; :: 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 number st 0 < y holds
ex x being real number st
( x in A & x < a + y )

proof

let y be real number ; :: thesis: ( 0 < y implies ex x being real number st
( x in A & x < a + y ) )
assume A9: 0 < y ; :: thesis: ex x being real number 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:31, XXREAL_1:1; :: thesis: verum

end;

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