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: 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 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 2;
then consider r1 being Real such that
A5: ( r1 = r & a < r1 & r1 < b ) ;
thus b >= r by A5; :: thesis: verum

end;

A6: ( a < (a + b) / 2 & (a + b) / 2 < b ) by A1, XREAL_1:228;
then A7: (a + b) / 2 in { l where l is Real : ( a < l & l < b ) } ;
then A8: (a + b) / 2 in ].a,b.[ by RCOMP_1:def 2;
then A9: ( ex r being real number st r in ].a,b.[ & ].a,b.[ is bounded_below ) by A2, SEQ_4:def 2;
A10: ( ex r being real number st r in ].a,b.[ & ].a,b.[ is bounded_above ) by A4, A8, SEQ_4:def 1;
A11: 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 consider r1 being Real such that
A12: ( r1 = r & a < r1 & r1 < b ) ;
thus a <= r by A12; :: thesis: verum

end;

A13: 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
A14: 0 < s and
A15: 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 a + s >= b ; :: thesis: contradiction

then ( (a + b) / 2 in ].a,b.[ & (a + b) / 2 < a + s ) by A6, A7, RCOMP_1:def 2, XXREAL_0:2;
hence contradiction by A15; :: thesis: verum

end;

suppose A16: a + s < b ; :: thesis: contradiction

A17: a < a + s by A14, XREAL_1:31;
then A18: a < (a + (a + s)) / 2 by XREAL_1:228;
A19: (a + (a + s)) / 2 < a + s by A17, XREAL_1:228;
then (a + (a + s)) / 2 < b by A16, XXREAL_0:2;
then (a + (a + s)) / 2 in { r where r is Real : ( a < r & r < b ) } by A18;
then (a + (a + s)) / 2 in ].a,b.[ by RCOMP_1:def 2;
hence contradiction by A15, A19; :: thesis: verum

end;

end;

end;

A20: 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 consider r1 being Real such that
A21: ( r1 = r & a < r1 & r1 < b ) ;
thus b >= r by A21; :: 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 that
A22: 0 < s and
A23: 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 b - s <= a ; :: thesis: contradiction

then ( (a + b) / 2 in ].a,b.[ & (a + b) / 2 > b - s ) by A6, A7, RCOMP_1:def 2, XXREAL_0:2;
hence contradiction by A23; :: thesis: verum

end;

suppose A24: b - s > a ; :: thesis: contradiction

A25: b - s < b - 0 by A22, XREAL_1:17;
then b - s < (b + (b - s)) / 2 by XREAL_1:228;
then A26: a < (b + (b - s)) / 2 by A24, XXREAL_0:2;
A27: (b + (b - s)) / 2 > b - s by A25, XREAL_1:228;
(b + (b - s)) / 2 < b by A25, XREAL_1:228;
then (b + (b - s)) / 2 in { r where r is Real : ( a < r & r < b ) } by A26;
then (b + (b - s)) / 2 in ].a,b.[ by RCOMP_1:def 2;
hence contradiction by A23, A27; :: thesis: verum

end;

end;

end;

hence ( inf ].a,b.[ = a & sup ].a,b.[ = b ) by A9, A10, A11, A13, A20, SEQ_4:def 4, SEQ_4:def 5; :: thesis: verum