let S be RealNormSpace; :: thesis: for p being Element of S
for r being Real st 0 < r holds
( p in Ball (p,r) & p in cl_Ball (p,r) )
let p be Element of S; :: thesis: for r being Real st 0 < r holds
( p in Ball (p,r) & p in cl_Ball (p,r) )
let r be Real; :: thesis: ( 0 < r implies ( p in Ball (p,r) & p in cl_Ball (p,r) ) )
assume A1: 0 < r ; :: thesis: ( p in Ball (p,r) & p in cl_Ball (p,r) )
A2: ||.(p - p).|| = ||.(0. S).|| by RLVECT_1:15
.= 0 ;
hence p in Ball (p,r) by A1; :: thesis: p in cl_Ball (p,r)
thus p in cl_Ball (p,r) by A1, A2; :: thesis: verum