let S be Subset of (TOP-REAL 2); :: thesis: ( S is bounded implies proj1 .: S is real-bounded )
assume S is bounded ; :: thesis: proj1 .: 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 `1) - r).|,|.((p `1) + r).|);

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

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

end;

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

proof

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

end;

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