let a, b be Real; ( a <= b implies ( lower_bound [.a,b.] = a & upper_bound [.a,b.] = b ) )
assume A1:
a <= b
; ( lower_bound [.a,b.] = a & upper_bound [.a,b.] = b )
set X = [.a,b.];
A2:
a in { l where l is Real : ( a <= l & l <= b ) }
by A1;
A3:
for s being Real st 0 < s holds
ex r being Real st
( r in [.a,b.] & r < a + s )
A6:
b in { l1 where l1 is Real : ( a <= l1 & l1 <= b ) }
by A1;
A7:
for s being Real st 0 < s holds
ex r being Real st
( r in [.a,b.] & b - s < r )
A10:
for r being Real st r in [.a,b.] holds
a <= r
b is UpperBound of [.a,b.]
then A11:
[.a,b.] is bounded_above
;
a is LowerBound of [.a,b.]
then A12:
[.a,b.] is bounded_below
;
A13:
for r being Real st r in [.a,b.] holds
b >= r
a in [.a,b.]
by A2, RCOMP_1:def 1;
hence
( lower_bound [.a,b.] = a & upper_bound [.a,b.] = b )
by A12, A11, A10, A3, A13, A7, SEQ_4:def 1, SEQ_4:def 2; verum