let W be Subset of (Euclid 1); :: thesis: for a being Real
for P being Subset of (TOP-REAL 1) st W = { q where q is Point of (TOP-REAL 1) : ex r being Real st
( q = <*r*> & r > a ) } & P = W holds
( P is connected & not W is bounded )
let a be Real; :: thesis: for P being Subset of (TOP-REAL 1) st W = { q where q is Point of (TOP-REAL 1) : ex r being Real st
( q = <*r*> & r > a ) } & P = W holds
( P is connected & not W is bounded )
let P be Subset of (TOP-REAL 1); :: thesis: ( W = { q where q is Point of (TOP-REAL 1) : ex r being Real st
( q = <*r*> & r > a ) } & P = W implies ( P is connected & not W is bounded ) )
assume A1: ( W = { q where q is Point of (TOP-REAL 1) : ex r being Real st
( q = <*r*> & r > a ) } & P = W ) ; :: thesis: ( P is connected & not W is bounded )
hence P is connected by Th63, JORDAN1:6; :: thesis: not W is bounded

now

abs a >= 0 by COMPLEX1:46;
then A2: ((abs a) + (abs a)) + (abs a) >= 0 + (abs a) by XREAL_1:6;
assume W is bounded ; :: thesis: contradiction
then consider r being Real such that
A3: 0 < r and
A4: for x, y being Point of (Euclid 1) st x in W & y in W holds
dist (x,y) <= r by TBSP_1:def 7;
A5: (r + (abs a)) * (1.REAL 1) = (r + (abs a)) * <*1*> by FINSEQ_2:59
.= <*((r + (abs a)) * 1)*> by RVSUM_1:47 ;
reconsider z2 = (r + (abs a)) * (1.REAL 1) as Point of (Euclid 1) by FINSEQ_2:131;
( a <= abs a & 0 + (abs a) < r + (abs a) ) by A3, ABSVALUE:4, XREAL_1:6;
then a < r + (abs a) by XXREAL_0:2;
then A6: (r + (abs a)) * (1.REAL 1) in W by A1, A5;
A7: (3 * (r + (abs a))) * (1.REAL 1) = (3 * (r + (abs a))) * <*1*> by FINSEQ_2:59
.= <*((3 * (r + (abs a))) * 1)*> by RVSUM_1:47 ;
reconsider z1 = (3 * (r + (abs a))) * (1.REAL 1) as Point of (Euclid 1) by FINSEQ_2:131;
dist (z1,z2) = |.(((3 * (r + (abs a))) * (1.REAL 1)) - ((r + (abs a)) * (1.REAL 1))).| by JGRAPH_1:28
.= |.(((((r + (abs a)) + (r + (abs a))) + (r + (abs a))) - (r + (abs a))) * (1.REAL 1)).| by EUCLID:50
.= (abs ((r + (abs a)) + (r + (abs a)))) * |.(1.REAL 1).| by TOPRNS_1:7
.= (abs ((r + (abs a)) + (r + (abs a)))) * (sqrt 1) by Th35 ;
then A8: (r + (abs a)) + (r + (abs a)) <= dist (z1,z2) by ABSVALUE:4, SQUARE_1:18;
A9: 0 <= abs a by COMPLEX1:46;
then (r + (abs a)) + 0 < (r + (abs a)) + (r + (abs a)) by A3, XREAL_1:6;
then A10: r + (abs a) < dist (z1,z2) by A8, XXREAL_0:2;
r + 0 <= r + (abs a) by A9, XREAL_1:6;
then A11: r < dist (z1,z2) by A10, XXREAL_0:2;
3 * r > 0 by A3, XREAL_1:129;
then ( a <= abs a & 0 + (abs a) < (3 * r) + (3 * (abs a)) ) by A2, ABSVALUE:4, XREAL_1:8;
then a < 3 * (r + (abs a)) by XXREAL_0:2;
then (3 * (r + (abs a))) * (1.REAL 1) in W by A1, A7;
hence contradiction by A4, A6, A11; :: thesis: verum

end;

hence not W is bounded ; :: thesis: verum