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 by A1, TOPREAL3:21;

hence A is connected ; :: thesis: verum

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 by A1, TOPREAL3:21;

hence A is connected ; :: thesis: verum