let X be Subset of REAL; :: thesis: ( X is bounded iff ex s being real number st
( 0 < s & ( for r being real number st r in X holds
abs r < s ) ) )
thus ( X is bounded implies ex s being real number st
( 0 < s & ( for r being real number st r in X holds
abs r < s ) ) ) :: thesis: ( ex s being real number st
( 0 < s & ( for r being real number st r in X holds
abs r < s ) ) implies X is bounded )

proof

assume A1: X is bounded ; :: thesis: ex s being real number st
( 0 < s & ( for r being real number st r in X holds
abs r < s ) )
then consider s1 being real number such that
A2: s1 is UpperBound of X by XXREAL_2:def 10;
A3: for r being real number st r in X holds
r <= s1 by A2, XXREAL_2:def 1;
consider s2 being real number such that
A4: s2 is LowerBound of X by A1, XXREAL_2:def 9;
A5: for r being real number st r in X holds
s2 <= r by A4, XXREAL_2:def 2;
take s = ((abs s1) + (abs s2)) + 1; :: thesis: ( 0 < s & ( for r being real number st r in X holds
abs r < s ) )
A6: 0 <= abs s1 by COMPLEX1:46;
A7: 0 <= abs s2 by COMPLEX1:46;
hence 0 < s by A6; :: thesis: for r being real number st r in X holds
abs r < s
let r be real number ; :: thesis: ( r in X implies abs r < s )
assume A8: r in X ; :: thesis: abs r < s
( s1 <= abs s1 & r <= s1 ) by A3, A8, ABSVALUE:4;
then r <= abs s1 by XXREAL_0:2;
then r + 0 <= (abs s1) + (abs s2) by A7, XREAL_1:7;
then A9: r < s by XREAL_1:8;
( - (abs s2) <= s2 & s2 <= r ) by A5, A8, ABSVALUE:4;
then - (abs s2) <= r by XXREAL_0:2;
then (- (abs s1)) + (- (abs s2)) <= 0 + r by A6, XREAL_1:7;
then A10: ((- (abs s1)) - (abs s2)) + (- 1) < r + 0 by XREAL_1:8;
((- (abs s1)) - (abs s2)) - 1 = - (((abs s1) + (abs s2)) + 1) ;
hence abs r < s by A9, A10, SEQ_2:1; :: thesis: verum

end;

given s being real number such that 0 < s and
A11: for r being real number st r in X holds
abs r < s ; :: thesis: X is bounded
thus X is bounded_below :: according to XXREAL_2:def 11 :: thesis: X is bounded_above

proof

take - s ; :: according to XXREAL_2:def 9 :: thesis: - s is LowerBound of X
let r be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( not r in X or - s <= r )
assume A12: r in X ; :: thesis: - s <= r
then reconsider r = r as real number ;
abs r < s by A11, A12;
then A13: - s < - (abs r) by XREAL_1:24;
- (abs r) <= r by ABSVALUE:4;
hence - s <= r by A13, XXREAL_0:2; :: thesis: verum

end;

take s ; :: according to XXREAL_2:def 10 :: thesis: s is UpperBound of X
let r be ext-real number ; :: according to XXREAL_2:def 1 :: thesis: ( not r in X or r <= s )
assume A14: r in X ; :: thesis: r <= s
then reconsider r = r as real number ;
r <= abs r by ABSVALUE:4;
hence r <= s by A11, A14, XXREAL_0:2; :: thesis: verum