let a, b be Real; :: 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: 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 )
proof
let s be Real; :: thesis: ( 0 < s implies ex r being Real st
( r in [.a,b.] & r < a + s ) )
assume A4: 0 < s ; :: thesis: ex r being Real st
( r in [.a,b.] & r < a + s )
A5: a in [.a,b.] by A2, RCOMP_1:def 1;
assume for r being Real st r in [.a,b.] holds
r >= a + s ; :: thesis: contradiction
hence contradiction by A4, A5, XREAL_1:29; :: thesis: verum
end;
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 )
proof
let s be Real; :: thesis: ( 0 < s implies ex r being Real st
( r in [.a,b.] & b - s < r ) )
assume A8: 0 < s ; :: thesis: ex r being Real st
( r in [.a,b.] & b - s < r )
A9: b in [.a,b.] by A6, RCOMP_1:def 1;
assume for r being Real st r in [.a,b.] holds
r <= b - s ; :: thesis: contradiction
hence contradiction by A8, A9, XREAL_1:44; :: thesis: verum
end;
A10: for r being Real st r in [.a,b.] holds
a <= r
proof
let r be Real; :: 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 ex r1 being Real st
( r1 = r & a <= r1 & r1 <= b ) ;
hence a <= r ; :: thesis: verum
end;
b is UpperBound of [.a,b.]
proof
let r be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not r in [.a,b.] or r <= b )
assume r in [.a,b.] ; :: thesis: r <= b
then r in { l where l is Real : ( a <= l & l <= b ) } by RCOMP_1:def 1;
then ex r1 being Real st
( r1 = r & a <= r1 & r1 <= b ) ;
hence r <= b ; :: thesis: verum
end;
then A11: [.a,b.] is bounded_above ;
a is LowerBound of [.a,b.]
proof
let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r in [.a,b.] or 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 ex r1 being Real st
( r1 = r & a <= r1 & r1 <= b ) ;
hence a <= r ; :: thesis: verum
end;
then A12: [.a,b.] is bounded_below ;
A13: for r being Real st r in [.a,b.] holds
b >= r
proof
let r be Real; :: 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 ex r1 being Real st
( r1 = r & a <= r1 & r1 <= b ) ;
hence b >= r ; :: thesis: verum
end;
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; :: thesis: verum