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 & A = [.a,b.] ) by Def1;
( a = lower_bound A & b = upper_bound A )

proof

A3: 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 A4: x in A ; :: thesis: a <= x
A = { y where y is Real : ( a <= y & y <= b ) } by A1, RCOMP_1:def 1;
then ex y being Real st
( x = y & a <= y & y <= b ) by A4;
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 A5: 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, A5, XREAL_1:31, XXREAL_1:1; :: thesis: verum

end;

hence a = lower_bound A by A3, SEQ_4:def 5; :: thesis: b = upper_bound A
A7: 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 A8: x in A ; :: thesis: x <= b
A = { y where y is Real : ( a <= y & y <= b ) } by A1, RCOMP_1:def 1;
then ex y being Real st
( x = y & a <= y & y <= b ) by A8;
hence x <= b ; :: thesis: verum

end;

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 A9: 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 A9, XREAL_1:31;
then b - y < (b + y) - y by XREAL_1:11;
hence ( b in A & b - y < b ) by A1, XXREAL_1:1; :: thesis: verum

end;

hence b = upper_bound A by A7, SEQ_4:def 4; :: thesis: verum

end;

hence A = [.(lower_bound A),(upper_bound A).] by A1; :: thesis: verum