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).|);

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).|)

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 )

then A6:
max (|.((p `2) - r).|,|.((p `2) + r).|) > 0
by XXREAL_0:30;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;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

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

hence
proj2 .: S is real-bounded
by A6, SEQ_4:4; :: thesis: verum
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;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