let S be Subset of (TOP-REAL 2); :: thesis: ( S is bounded implies proj2 .: S is real-bounded )
assume S is bounded ; :: thesis: proj2 .: S is real-bounded
then reconsider C = S as bounded Subset of (Euclid 2) by JORDAN2C:11;
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 3;
reconsider P = Ball (x,r) as Subset of (TOP-REAL 2) by TOPREAL3:8;
reconsider p = x as Point of (TOP-REAL 2) by TOPREAL3:8;
set t = max (|.((p `2) - r).|,|.((p `2) + r).|);

now :: thesis: ( |.((p `2) - r).| <= 0 implies not |.((p `2) + r).| <= 0 )

assume that
A3: |.((p `2) - r).| <= 0 and
A4: |.((p `2) + r).| <= 0 ; :: thesis: contradiction
|.((p `2) - r).| = 0 by A3, COMPLEX1:46;
then |.(r - (p `2)).| = 0 by UNIFORM1:11;
then A5: r - (p `2) = 0 by ABSVALUE:2;
|.((p `2) + r).| = 0 by A4, COMPLEX1:46;
hence contradiction by A1, A5, ABSVALUE:2; :: thesis: verum

end;

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

proof

let s be Real; :: thesis: ( s in proj2 .: S implies |.s.| < max (|.((p `2) - r).|,|.((p `2) + r).|) )
proj2 .: S c= proj2 .: P by A2, RELAT_1:123;
hence ( s in proj2 .: S implies |.s.| < max (|.((p `2) - r).|,|.((p `2) + r).|) ) by A7, Th3; :: thesis: verum

end;

hence proj2 .: S is real-bounded by A6, SEQ_4:4; :: thesis: verum