let z be Point of [:RNS_Real,RNS_Real:]; :: thesis: 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) )
let r be Real; :: thesis: ( 0 < r implies 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) ) )
assume A1: 0 < r ; :: thesis: 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) )
consider xx, yy being Point of RNS_Real such that
A2: z = [xx,yy] by PRVECT_3:18;
reconsider x = xx, y = yy as Real ;
consider s being Real such that
A3: ( 0 < s & s < r & [:(Ball (xx,s)),(Ball (yy,s)):] c= Ball (z,r) ) by A1, A2, NDIFF_8:22;
( Ball (xx,s) = ].(x - s),(x + s).[ & Ball (yy,s) = ].(y - s),(y + s).[ ) by Th12;
hence 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) ) by A2, A3; :: thesis: verum