let V be RealUnitarySpace; :: thesis: for v being VECTOR of V
for r being Real st r = 0 holds
Ball (v,r) is empty
let v be VECTOR of V; :: thesis: for r being Real st r = 0 holds
Ball (v,r) is empty
let r be Real; :: thesis: ( r = 0 implies Ball (v,r) is empty )
assume A1: r = 0 ; :: thesis: Ball (v,r) is empty
assume not Ball (v,r) is empty ; :: thesis: contradiction
then consider u being object such that
A2: u in Ball (v,r) ;
u in { y where y is Point of V : ||.(v - y).|| < r } by A2, BHSP_2:def 5;
then ex w being Point of V st
( u = w & ||.(v - w).|| < r ) ;
hence contradiction by A1, BHSP_1:28; :: thesis: verum