theorem :: RUSUB_5:45

for V being RealUnitarySpace
for v being VECTOR of V
for r being Real st the carrier of V <> {(0. V)} & r > 0 holds
not Sphere (v,r) is empty