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:9; :: thesis: not W is bounded
now assume
W is
bounded
;
:: thesis: contradictionthen consider r being
Real such that A2:
(
0 < r & ( for
x,
y being
Point of
(Euclid 1) st
x in W &
y in W holds
dist x,
y <= r ) )
by TBSP_1:def 9;
A3:
a <= abs a
by ABSVALUE:11;
A4:
abs a >= 0
by COMPLEX1:132;
A5:
((abs a) + (abs a)) + (abs a) >= 0 + (abs a)
by A4, XREAL_1:8;
3
* r > 0
by A2, XREAL_1:131;
then
0 + (abs a) < (3 * r) + (3 * (abs a))
by A5, XREAL_1:10;
then A6:
a < 3
* (r + (abs a))
by A3, XXREAL_0:2;
A7:
(3 * (r + (abs a))) * (1.REAL 1) =
(3 * (r + (abs a))) * <*1*>
by Lm1, EUCLID:69
.=
<*((3 * (r + (abs a))) * 1)*>
by Lm1, RVSUM_1:69
;
then A8:
(3 * (r + (abs a))) * (1.REAL 1) in W
by A1, A6;
reconsider z1 =
(3 * (r + (abs a))) * (1.REAL 1) as
Point of
(Euclid 1) by A7;
A9:
a <= abs a
by ABSVALUE:11;
0 + (abs a) < r + (abs a)
by A2, XREAL_1:8;
then A10:
a < r + (abs a)
by A9, XXREAL_0:2;
A11:
(r + (abs a)) * (1.REAL 1) =
(r + (abs a)) * <*1*>
by Lm1, EUCLID:69
.=
<*((r + (abs a)) * 1)*>
by Lm1, RVSUM_1:69
;
then A12:
(r + (abs a)) * (1.REAL 1) in W
by A1, A10;
reconsider z2 =
(r + (abs a)) * (1.REAL 1) as
Point of
(Euclid 1) by A11;
0 <= abs a
by COMPLEX1:132;
then A13:
r + 0 <= r + (abs a)
by XREAL_1:8;
dist z1,
z2 =
|.(((3 * (r + (abs a))) * (1.REAL 1)) - ((r + (abs a)) * (1.REAL 1))).|
by JGRAPH_1:45
.=
|.(((((r + (abs a)) + (r + (abs a))) + (r + (abs a))) - (r + (abs a))) * (1.REAL 1)).|
by EUCLID:54
.=
(abs ((r + (abs a)) + (r + (abs a)))) * |.(1.REAL 1).|
by TOPRNS_1:8
.=
(abs ((r + (abs a)) + (r + (abs a)))) * (sqrt 1)
by Th35
;
then A14:
(r + (abs a)) + (r + (abs a)) <= dist z1,
z2
by ABSVALUE:11, SQUARE_1:83;
(r + (abs a)) + 0 < (r + (abs a)) + (r + (abs a))
by A2, A13, XREAL_1:8;
then
r + (abs a) < dist z1,
z2
by A14, XXREAL_0:2;
then
r < dist z1,
z2
by A13, XXREAL_0:2;
hence
contradiction
by A2, A8, A12;
:: thesis: verum end;
hence
not W is bounded
; :: thesis: verum