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 set such that
A2: u in Ball v,r by XBOOLE_0:def 1;
u in { y where y is Point of V : ||.(v - y).|| < r } by A2, BHSP_2:def 5;
then consider w being Point of V such that
A3: ( u = w & ||.(v - w).|| < r ) ;
thus contradiction by A1, A3, BHSP_1:34; :: thesis: verum