let u be Point of [:RNS_Real,RNS_Real,RNS_Real:]; :: thesis: 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) )
let r be Real; :: thesis: ( 0 < r implies 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) ) )
assume A1: 0 < r ; :: thesis: 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) )
consider xx, yy, zz being Point of RNS_Real such that
A2: u = [xx,yy,zz] by PRVECT_4:9;
reconsider u1 = [xx,yy] as Point of [:RNS_Real,RNS_Real:] ;
consider s being Real such that
A3: ( 0 < s & s < r & [:(Ball (u1,s)),(Ball (zz,s)):] c= Ball (u,r) ) by NDIFF_8:22, A1, A2;
consider s1, x, y being Real such that
A4: ( 0 < s1 & s1 < s & u1 = [x,y] & [:].(x - s1),(x + s1).[,].(y - s1),(y + s1).[:] c= Ball (u1,s) ) by A3, MESFUN16:13;
A5: Ball (zz,s1) c= Ball (zz,s) by A4, NDIFF_8:15;
reconsider z = zz as Real ;
take s1 ; :: thesis: ex x, y, z being Real st
( 0 < s1 & s1 < r & u = [x,y,z] & [:].(x - s1),(x + s1).[,].(y - s1),(y + s1).[,].(z - s1),(z + s1).[:] c= Ball (u,r) )
take x ; :: thesis: ex y, z being Real st
( 0 < s1 & s1 < r & u = [x,y,z] & [:].(x - s1),(x + s1).[,].(y - s1),(y + s1).[,].(z - s1),(z + s1).[:] c= Ball (u,r) )
take y ; :: thesis: ex z being Real st
( 0 < s1 & s1 < r & u = [x,y,z] & [:].(x - s1),(x + s1).[,].(y - s1),(y + s1).[,].(z - s1),(z + s1).[:] c= Ball (u,r) )
take z ; :: thesis: ( 0 < s1 & s1 < r & u = [x,y,z] & [:].(x - s1),(x + s1).[,].(y - s1),(y + s1).[,].(z - s1),(z + s1).[:] c= Ball (u,r) )
thus 0 < s1 by A4; :: thesis: ( s1 < r & u = [x,y,z] & [:].(x - s1),(x + s1).[,].(y - s1),(y + s1).[,].(z - s1),(z + s1).[:] c= Ball (u,r) )
thus s1 < r by A3, A4, XXREAL_0:2; :: thesis: ( u = [x,y,z] & [:].(x - s1),(x + s1).[,].(y - s1),(y + s1).[,].(z - s1),(z + s1).[:] c= Ball (u,r) )
thus u = [x,y,z] by A2, A4; :: thesis: [:].(x - s1),(x + s1).[,].(y - s1),(y + s1).[,].(z - s1),(z + s1).[:] c= Ball (u,r)
Ball (zz,s1) = ].(z - s1),(z + s1).[ by MESFUN16:12;
then [:[:].(x - s1),(x + s1).[,].(y - s1),(y + s1).[:],].(z - s1),(z + s1).[:] c= [:(Ball (u1,s)),(Ball (zz,s)):] by A4, A5, ZFMISC_1:96;
hence [:].(x - s1),(x + s1).[,].(y - s1),(y + s1).[,].(z - s1),(z + s1).[:] c= Ball (u,r) by A3; :: thesis: verum