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