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.[;
reconsider a = a, b = b as Real ;
A2: (a + b) / 2 < b by A1, XREAL_1:226;
A3: a < (a + b) / 2 by A1, XREAL_1:226;
then A4: (a + b) / 2 in { l where l is Real : ( a < l & l < b ) } by A2;
A5: 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 that
A6: 0 < s and
A7: for r being Real st r in ].a,b.[ holds
r >= a + s ; :: thesis: contradiction
reconsider s = s as Real ;
per cases ( a + s >= b or a + s < b ) ;
suppose A8: a + s >= b ; :: thesis: contradiction
A9: (a + b) / 2 in ].a,b.[ by A4, RCOMP_1:def 2;
(a + b) / 2 < a + s by A2, A8, XXREAL_0:2;
hence contradiction by A7, A9; :: thesis: verum
end;
suppose A10: a + s < b ; :: thesis: contradiction
A11: a < a + s by A6, XREAL_1:29;
then (a + (a + s)) / 2 < a + s by XREAL_1:226;
then A12: (a + (a + s)) / 2 < b by A10, XXREAL_0:2;
a < (a + (a + s)) / 2 by A11, XREAL_1:226;
then (a + (a + s)) / 2 in { r where r is Real : ( a < r & r < b ) } by A12;
then (a + (a + s)) / 2 in ].a,b.[ by RCOMP_1:def 2;
hence contradiction by A7, A11, XREAL_1:226; :: thesis: verum
end;
end;
end;
A13: 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 that
A14: 0 < s and
A15: for r being Real st r in ].a,b.[ holds
r <= b - s ; :: thesis: contradiction
reconsider s = s as Real ;
per cases ( b - s <= a or b - s > a ) ;
suppose A18: b - s > a ; :: thesis: contradiction
A19: b - s < b - 0 by A14, XREAL_1:15;
then b - s < (b + (b - s)) / 2 by XREAL_1:226;
then A20: a < (b + (b - s)) / 2 by A18, XXREAL_0:2;
(b + (b - s)) / 2 < b by A19, XREAL_1:226;
then (b + (b - s)) / 2 in { r where r is Real : ( a < r & r < b ) } by A20;
then (b + (b - s)) / 2 in ].a,b.[ by RCOMP_1:def 2;
hence contradiction by A15, A19, XREAL_1:226; :: thesis: verum
end;
end;
end;
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 2;
then ex r1 being Real st
( r1 = r & a < r1 & r1 < b ) ;
hence a <= r ; :: thesis: verum
end;
then A21: ].a,b.[ is bounded_below ;
A22: 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 2;
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 2;
then ex r1 being Real st
( r1 = r & a < r1 & r1 < b ) ;
hence r <= b ; :: thesis: verum
end;
then A23: ].a,b.[ is bounded_above ;
A24: 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 2;
then ex r1 being Real st
( r1 = r & a < r1 & r1 < b ) ;
hence b >= r ; :: thesis: verum
end;
(a + b) / 2 in ].a,b.[ by A4, RCOMP_1:def 2;
hence ( lower_bound ].a,b.[ = a & upper_bound ].a,b.[ = b ) by A21, A23, A22, A5, A24, A13, SEQ_4:def 1, SEQ_4:def 2; :: thesis: verum