let a, b be real number ; :: thesis: ( a <= b implies ( lower_bound [.a,b.] = a & upper_bound [.a,b.] = b ) )
assume A1: a <= b ; :: thesis: ( lower_bound [.a,b.] = a & upper_bound [.a,b.] = b )
set X = [.a,b.];
A2: ex p being real number st
for r being real number st r in [.a,b.] holds
p <= r

proof

take a ; :: thesis: for r being real number st r in [.a,b.] holds
a <= r
let r be real number ; :: thesis: ( r in [.a,b.] implies a <= r )
assume r in [.a,b.] ; :: thesis: a <= r
then r in { l where l is Real : ( a <= l & l <= b ) } by RCOMP_1:def 1;
then consider r1 being Real such that
A3: ( r1 = r & a <= r1 & r1 <= b ) ;
thus a <= r by A3; :: thesis: verum

end;

A4: ex p being real number st
for r being real number st r in [.a,b.] holds
p >= r

proof

take b ; :: thesis: for r being real number st r in [.a,b.] holds
b >= r
let r be real number ; :: thesis: ( r in [.a,b.] implies b >= r )
assume r in [.a,b.] ; :: thesis: b >= r
then r in { l where l is Real : ( a <= l & l <= b ) } by RCOMP_1:def 1;
then consider r1 being Real such that
A5: ( r1 = r & a <= r1 & r1 <= b ) ;
thus b >= r by A5; :: thesis: verum

end;

( a is Real & b is Real ) by XREAL_0:def 1;
then A6: ( a in { l where l is Real : ( a <= l & l <= b ) } & b in { l1 where l1 is Real : ( a <= l1 & l1 <= b ) } ) by A1;
then A7: ( a in [.a,b.] & b in [.a,b.] ) by RCOMP_1:def 1;
then A8: ( ex r being real number st r in [.a,b.] & [.a,b.] is bounded_below ) by A2, SEQ_4:def 2;
A9: ( ex r being real number st r in [.a,b.] & [.a,b.] is bounded_above ) by A4, A7, SEQ_4:def 1;
A10: for r being real number st r in [.a,b.] holds
a <= r

proof

let r be real number ; :: thesis: ( r in [.a,b.] implies a <= r )
assume r in [.a,b.] ; :: thesis: a <= r
then r in { l where l is Real : ( a <= l & l <= b ) } by RCOMP_1:def 1;
then consider r1 being Real such that
A11: ( r1 = r & a <= r1 & r1 <= b ) ;
thus a <= r by A11; :: thesis: verum

end;

A12: for s being real number st 0 < s holds
ex r being real number st
( r in [.a,b.] & r < a + s )

proof

let s be real number ; :: thesis: ( 0 < s implies ex r being real number st
( r in [.a,b.] & r < a + s ) )
assume A13: 0 < s ; :: thesis: ex r being real number st
( r in [.a,b.] & r < a + s )
assume A14: for r being real number st r in [.a,b.] holds
r >= a + s ; :: thesis: contradiction
( a in [.a,b.] & a < a + s ) by A6, A13, RCOMP_1:def 1, XREAL_1:31;
hence contradiction by A14; :: thesis: verum

end;

A15: for r being real number st r in [.a,b.] holds
b >= r

proof

let r be real number ; :: thesis: ( r in [.a,b.] implies b >= r )
assume r in [.a,b.] ; :: thesis: b >= r
then r in { l where l is Real : ( a <= l & l <= b ) } by RCOMP_1:def 1;
then consider r1 being Real such that
A16: ( r1 = r & a <= r1 & r1 <= b ) ;
thus b >= r by A16; :: thesis: verum

end;

for s being real number st 0 < s holds
ex r being real number st
( r in [.a,b.] & b - s < r )

proof

let s be real number ; :: thesis: ( 0 < s implies ex r being real number st
( r in [.a,b.] & b - s < r ) )
assume A17: 0 < s ; :: thesis: ex r being real number st
( r in [.a,b.] & b - s < r )
assume A18: for r being real number st r in [.a,b.] holds
r <= b - s ; :: thesis: contradiction
( b in [.a,b.] & b - s < b ) by A6, A17, RCOMP_1:def 1, XREAL_1:46;
hence contradiction by A18; :: thesis: verum

end;

hence ( lower_bound [.a,b.] = a & upper_bound [.a,b.] = b ) by A8, A9, A10, A12, A15, SEQ_4:def 4, SEQ_4:def 5; :: thesis: verum