theorem Th13: :: MESFUN16:13

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