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 r <= 0 ; :: thesis: (Ball (x,r)) ` is connected Subset of (TOP-REAL 2)

then Ball (x,r) = {} (TOP-REAL 2) by TBSP_1:12;
then A1: (Ball (x,r)) ` = [#] (TOP-REAL 2) by TOPREAL3:8;
thus (Ball (x,r)) ` is connected Subset of (TOP-REAL 2) by A1; :: thesis: verum

end;

suppose A2: r > 0 ; :: thesis: (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; :: thesis: verum

end;

end;