let A be closed-interval Subset of REAL ; :: thesis: ex a, b being Real st
( a <= b & a = lower_bound A & b = upper_bound A )
consider a, b being Real such that
A1: ( a <= b & A = [.a,b.] ) by Def1;
A2: ( a = lower_bound A & b = upper_bound A )

proof

A4: 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 x in A ; :: thesis: a <= x
then x in { 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 ) ;
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 A4, 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 x in A ; :: thesis: x <= b
then x in { 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 ) ;
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 A8: 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 A8, 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;

take a ; :: thesis: ex b being Real st
( a <= b & a = lower_bound A & b = upper_bound A )
take b ; :: thesis: ( a <= b & a = lower_bound A & b = upper_bound A )
thus ( a <= b & a = lower_bound A & b = upper_bound A ) by A1, A2; :: thesis: verum