let S be Subset of (); :: thesis: ( S is bounded implies proj2 .: S is real-bounded )
assume S is bounded ; :: thesis:
then reconsider C = S as bounded Subset of () by JORDAN2C:11;
consider r being Real, x being Point of () 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 () by TOPREAL3:8;
reconsider p = x as Point of () 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 ;
then |.(r - (p `2)).| = 0 by UNIFORM1:11;
then A5: r - (p `2) = 0 by ABSVALUE:2;
|.((p `2) + r).| = 0 by ;
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 ;
hence ( s in proj2 .: S implies |.s.| < max (|.((p `2) - r).|,|.((p `2) + r).|) ) by ; :: thesis: verum
end;
hence proj2 .: S is real-bounded by ; :: thesis: verum