let a, b be real number ; :: thesis: ( a < b implies ( inf ].a,b.[ = a & sup ].a,b.[ = b ) )
assume A1: a < b ; :: thesis: ( inf ].a,b.[ = a & sup ].a,b.[ = b )
set X = ].a,b.[;
reconsider a = a, b = b as Real by XREAL_0:def 1;
A2: (a + b) / 2 < b by A1, XREAL_1:228;
A3: a < (a + b) / 2 by A1, XREAL_1:228;
then A4: (a + b) / 2 in { l where l is Real : ( a < l & l < b ) } by A2;
A5: 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 that
A6: 0 < s and
A7: for r being real number st r in ].a,b.[ holds
r >= a + s ; :: thesis: contradiction
reconsider s = s as Real by XREAL_0:def 1;
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:31;
then (a + (a + s)) / 2 < a + s by XREAL_1:228;
then A12: (a + (a + s)) / 2 < b by A10, XXREAL_0:2;
a < (a + (a + s)) / 2 by A11, XREAL_1:228;
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:228; :: thesis: verum
end;
end;
end;
A13: 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 that
A14: 0 < s and
A15: for r being real number st r in ].a,b.[ holds
r <= b - s ; :: thesis: contradiction
reconsider s = s as Real by XREAL_0:def 1;
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:17;
then b - s < (b + (b - s)) / 2 by XREAL_1:228;
then A20: a < (b + (b - s)) / 2 by A18, XXREAL_0:2;
(b + (b - s)) / 2 < b by A19, XREAL_1:228;
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:228; :: thesis: verum
end;
end;
end;
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 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 by SEQ_4:def 2;
A22: 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 2;
then ex r1 being Real st
( r1 = r & a < r1 & r1 < b ) ;
hence a <= r ; :: thesis: verum
end;
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 2;
then ex r1 being Real st
( r1 = r & a < r1 & r1 < b ) ;
hence b >= r ; :: thesis: verum
end;
then A23: ].a,b.[ is bounded_above by SEQ_4:def 1;
A24: 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 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 ( inf ].a,b.[ = a & sup ].a,b.[ = b ) by A21, A23, A22, A5, A24, A13, SEQ_4:def 4, SEQ_4:def 5; :: thesis: verum