let r be Real; for x being Point of (Euclid 2) holds (Ball (x,r)) ` is connected Subset of (TOP-REAL 2)
let x be Point of (Euclid 2); (Ball (x,r)) ` is connected Subset of (TOP-REAL 2)
set C = (Ball (x,r)) ` ;
per cases
( r <= 0 or r > 0 )
;
suppose A2:
r > 0
;
(Ball (x,r)) ` is connected Subset of (TOP-REAL 2)reconsider q =
x as
Point of
(TOP-REAL 2) by TOPREAL3:8;
reconsider y =
|[0,0]| as
Point of
(Euclid 2) by TOPREAL3:8;
reconsider Q =
Ball (
x,
r),
J =
Ball (
y,1) as
Subset of
(TOP-REAL 2) by TOPREAL3:8;
A3:
Q = (AffineMap (r,(q `1),r,(q `2))) .: J
by A2, Th35;
reconsider P =
Q ` ,
K =
J ` as
Subset of
(TOP-REAL 2) ;
A4:
K =
(REAL 2) \ (Ball (y,1))
by TOPREAL3:8
.=
(REAL 2) \ { q1 where q1 is Point of (TOP-REAL 2) : |.q1.| < 1 }
by Th31
;
(
AffineMap (
r,
(q `1),
r,
(q `2)) is
one-to-one &
AffineMap (
r,
(q `1),
r,
(q `2)) is
onto )
by A2, Th36, JGRAPH_2:44;
then
( the
carrier of
(TOP-REAL 2) = the
carrier of
(Euclid 2) &
P = (AffineMap (r,(q `1),r,(q `2))) .: K )
by A3, Th5, TOPREAL3:8;
hence
(Ball (x,r)) ` is
connected Subset of
(TOP-REAL 2)
by A4, JORDAN2C:53, TOPS_2:61;
verum end;