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