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
B2: s1 is UpperBound of X by XXREAL_2:def 10;
A2: for r being real number st r in X holds
r <= s1 by B2, XXREAL_2:def 1;
consider s2 being real number such that
B3: s2 is LowerBound of X by A1, XXREAL_2:def 9;
A3: for r being real number st r in X holds
s2 <= r by B3, 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 ) )
A4: 0 <= abs s1 by COMPLEX1:132;
A5: 0 <= abs s2 by COMPLEX1:132;
hence 0 < s by A4; :: 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 A6: r in X ; :: thesis: abs r < s
( s1 <= abs s1 & r <= s1 ) by A2, A6, ABSVALUE:11;
then r <= abs s1 by XXREAL_0:2;
then r + 0 <= (abs s1) + (abs s2) by A5, XREAL_1:9;
then A7: r < s by XREAL_1:10;
( - (abs s2) <= s2 & s2 <= r ) by A3, A6, ABSVALUE:11;
then - (abs s2) <= r by XXREAL_0:2;
then (- (abs s1)) + (- (abs s2)) <= 0 + r by A4, XREAL_1:9;
then A8: ((- (abs s1)) - (abs s2)) + (- 1) < r + 0 by XREAL_1:10;
((- (abs s1)) - (abs s2)) - 1 = - (((abs s1) + (abs s2)) + 1) ;
hence abs r < s by A7, A8, SEQ_2:9; :: thesis: verum

end;

given s being real number such that 0 < s and
A9: 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 Z: r in X ; :: thesis: - s <= r
then reconsider r = r as real number ;
abs r < s by A9, Z;
then A10: - s < - (abs r) by XREAL_1:26;
- (abs r) <= r by ABSVALUE:11;
hence - s <= r by A10, 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 Z: r in X ; :: thesis: r <= s
then reconsider r = r as real number ;
r <= abs r by ABSVALUE:11;
hence r <= s by A9, XXREAL_0:2, Z; :: thesis: verum