let S be Subset of (TOP-REAL 2); :: thesis: ( S is Bounded implies proj2 .: S is bounded )
assume S is Bounded ; :: thesis: proj2 .: S is bounded
then reconsider C = S as bounded Subset of (Euclid 2) by JORDAN2C:def 2;
consider r being Real, x being Point of (Euclid 2) such that
A1: 0 < r and
A2: C c= Ball (x,r) by METRIC_6:def 10;
reconsider P = Ball (x,r) as Subset of (TOP-REAL 2) by TOPREAL3:13;
reconsider p = x as Point of (TOP-REAL 2) by TOPREAL3:13;
set t = max ((abs ((p `2) - r)),(abs ((p `2) + r)));

now

assume that
A3: abs ((p `2) - r) <= 0 and
A4: abs ((p `2) + r) <= 0 ; :: thesis: contradiction
abs ((p `2) - r) = 0 by A3, COMPLEX1:132;
then abs (r - (p `2)) = 0 by UNIFORM1:13;
then A5: r - (p `2) = 0 by ABSVALUE:7;
abs ((p `2) + r) = 0 by A4, COMPLEX1:132;
hence contradiction by A1, A5, ABSVALUE:7; :: thesis: verum

end;

then A6: max ((abs ((p `2) - r)),(abs ((p `2) + r))) > 0 by XXREAL_0:30;
A7: proj2 .: P = ].((p `2) - r),((p `2) + r).[ by TOPREAL6:52;
for s being real number st s in proj2 .: S holds
abs s < max ((abs ((p `2) - r)),(abs ((p `2) + r)))

proof

let s be real number ; :: thesis: ( s in proj2 .: S implies abs s < max ((abs ((p `2) - r)),(abs ((p `2) + r))) )
proj2 .: S c= proj2 .: P by A2, RELAT_1:156;
hence ( s in proj2 .: S implies abs s < max ((abs ((p `2) - r)),(abs ((p `2) + r))) ) by A7, Th12; :: thesis: verum

end;

hence proj2 .: S is bounded by A6, SEQ_4:14; :: thesis: verum