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:28; :: thesis: verum

end;

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