let A be non empty Subset of (TOP-REAL 2); :: thesis: for p being Element of (Euclid 2)
for r being Real st A = Ball (p,r) holds
A is connected
let p be Element of (Euclid 2); :: thesis: for r being Real st A = Ball (p,r) holds
A is connected
let r be Real; :: thesis: ( A = Ball (p,r) implies A is connected )
assume A1: A = Ball (p,r) ; :: thesis: A is connected
A is convex

proof

let w1, w2 be Point of (TOP-REAL 2); :: according to JORDAN1:def 1 :: thesis: ( not w1 in A or not w2 in A or LSeg (w1,w2) c= A )
assume that
A2: w1 in A and
A3: w2 in A ; :: thesis: LSeg (w1,w2) c= A
thus LSeg (w1,w2) c= A by A1, A2, A3, TOPREAL3:21; :: thesis: verum

end;

hence A is connected by JORDAN1:6; :: thesis: verum