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: for r being real number st r in X holds
r <= s1 by Def1;
consider s2 being real number such that
A3: for r being real number st r in X holds
s2 <= r by A1, Def2;
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

now

take g = - s; :: thesis: for r being real number st r in X holds
g <= r
let r be real number ; :: thesis: ( r in X implies g <= r )
assume r in X ; :: thesis: g <= r
then abs r < s by A9;
then A10: - s < - (abs r) by XREAL_1:26;
- (abs r) <= r by ABSVALUE:11;
hence g <= r by A10, XXREAL_0:2; :: thesis: verum

end;

then A11: X is bounded_below by Def2;

now

take g = s; :: thesis: for r being real number st r in X holds
r <= g
let r be real number ; :: thesis: ( r in X implies r <= g )
A12: r <= abs r by ABSVALUE:11;
assume r in X ; :: thesis: r <= g
hence r <= g by A9, A12, XXREAL_0:2; :: thesis: verum

end;

then X is bounded_above by Def1;
hence X is bounded by A11; :: thesis: verum