let n be Nat; :: thesis: for p being Point of (TOP-REAL n)

for r being Real st r > 0 holds

( not cl_Ball (p,r) is boundary & cl_Ball (p,r) is compact )

let p be Point of (TOP-REAL n); :: thesis: for r being Real st r > 0 holds

( not cl_Ball (p,r) is boundary & cl_Ball (p,r) is compact )

let r be Real; :: thesis: ( r > 0 implies ( not cl_Ball (p,r) is boundary & cl_Ball (p,r) is compact ) )

assume A1: r > 0 ; :: thesis: ( not cl_Ball (p,r) is boundary & cl_Ball (p,r) is compact )

Ball (p,r) c= Int (cl_Ball (p,r)) by TOPREAL9:16, TOPS_1:24;

hence ( not cl_Ball (p,r) is boundary & cl_Ball (p,r) is compact ) by A1; :: thesis: verum

for r being Real st r > 0 holds

( not cl_Ball (p,r) is boundary & cl_Ball (p,r) is compact )

let p be Point of (TOP-REAL n); :: thesis: for r being Real st r > 0 holds

( not cl_Ball (p,r) is boundary & cl_Ball (p,r) is compact )

let r be Real; :: thesis: ( r > 0 implies ( not cl_Ball (p,r) is boundary & cl_Ball (p,r) is compact ) )

assume A1: r > 0 ; :: thesis: ( not cl_Ball (p,r) is boundary & cl_Ball (p,r) is compact )

Ball (p,r) c= Int (cl_Ball (p,r)) by TOPREAL9:16, TOPS_1:24;

hence ( not cl_Ball (p,r) is boundary & cl_Ball (p,r) is compact ) by A1; :: thesis: verum