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 Th64, JORDAN1:9; :: thesis: not W is bounded
assume W is bounded ; :: thesis: contradiction
then 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 a < 3 * (r + (abs a)) by A3, XXREAL_0:2;
then A6: - a > - (3 * (r + (abs a))) by XREAL_1:26;
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 { q where q is Point of (TOP-REAL 1) : ex r being Real st
( q = <*r*> & r < - a ) } by 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 a < r + (abs a) by A9, XXREAL_0:2;
then A10: - a > - (r + (abs a)) by XREAL_1:26;
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
.= |.(((- (3 * (r + (abs a)))) - (- (r + (abs a)))) * (1.REAL 1)).| by EUCLID:54
.= |.(- (((- (3 * (r + (abs a)))) - (- (r + (abs a)))) * (1.REAL 1))).| by TOPRNS_1:27
.= |.((- ((- (3 * (r + (abs a)))) + (- (- (r + (abs a)))))) * (1.REAL 1)).| by EUCLID:44
.= (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 A1, A2, A8, A12; :: thesis: verum