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:17;
then (Ball (x,r)) ` = [#] (TOP-REAL 2) by TOPREAL3:13;
hence (Ball (x,r)) ` is connected Subset of (TOP-REAL 2) ; :: thesis: verum

end;

suppose A1: r > 0 ; :: thesis: (Ball (x,r)) ` is connected Subset of (TOP-REAL 2)

reconsider q = x as Point of (TOP-REAL 2) by TOPREAL3:13;
reconsider y = |[0,0]| as Point of (Euclid 2) by TOPREAL3:13;
reconsider Q = Ball (x,r), J = Ball (y,1) as Subset of (TOP-REAL 2) by TOPREAL3:13;
A2: Q = (AffineMap (r,(q `1),r,(q `2))) .: J by A1, Th35;
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 ;
( AffineMap (r,(q `1),r,(q `2)) is one-to-one & AffineMap (r,(q `1),r,(q `2)) is onto ) by A1, Th36, JGRAPH_2:54;
then ( the carrier of (TOP-REAL 2) = the carrier of (Euclid 2) & P = (AffineMap (r,(q `1),r,(q `2))) .: K ) by A2, Th5, TOPREAL3:13;
hence (Ball (x,r)) ` is connected Subset of (TOP-REAL 2) by A3, JORDAN2C:61, TOPS_2:75; :: thesis: verum

end;

end;