theorem Th5: :: MESFUN17:5

for u being Point of [:RNS_Real,RNS_Real,RNS_Real:]
for r being Real st 0 < r holds
ex s, x, y, z being Real st
( 0 < s & s < r & u = [x,y,z] & [:].(x - s),(x + s).[,].(y - s),(y + s).[,].(z - s),(z + s).[:] c= Ball (u,r) )