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
A7: s1 <= abs s1 by ABSVALUE:11;
r <= s1 by A2, A6;
then r <= abs s1 by A7, XXREAL_0:2;
then r + 0 <= (abs s1) + (abs s2) by A5, XREAL_1:9;
then A8: r < s by XREAL_1:10;
A9: - (abs s2) <= s2 by ABSVALUE:11;
s2 <= r by A3, A6;
then - (abs s2) <= r by A9, XXREAL_0:2;
then (- (abs s1)) + (- (abs s2)) <= 0 + r by A4, XREAL_1:9;
then A11: ((- (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 A8, A11, SEQ_2:9; :: thesis: verum

end;

given s being real number such that 0 < s and
A12: 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
r <= g
let r be real number ; :: thesis: ( r in X implies r <= g )
assume A13: r in X ; :: thesis: r <= g
r <= abs r by ABSVALUE:11;
hence r <= g by A12, A13, XXREAL_0:2; :: thesis: verum

end;

then A14: X is bounded_above by Def1;

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 A12;
then A15: - s < - (abs r) by XREAL_1:26;
- (abs r) <= r by ABSVALUE:11;
hence g <= r by A15, XXREAL_0:2; :: thesis: verum

end;

then X is bounded_below by Def2;
hence X is bounded by A14; :: thesis: verum