let z be Point of RNS_Real; :: thesis: for x, r being Real st x = z holds
Ball (z,r) = ].(x - r),(x + r).[
let x, r be Real; :: thesis: ( x = z implies Ball (z,r) = ].(x - r),(x + r).[ )
assume A1: x = z ; :: thesis: Ball (z,r) = ].(x - r),(x + r).[
for p being object holds
( p in Ball (z,r) iff p in ].(x - r),(x + r).[ )

proof

let p be object ; :: thesis: ( p in Ball (z,r) iff p in ].(x - r),(x + r).[ )

hereby :: thesis: ( p in ].(x - r),(x + r).[ implies p in Ball (z,r) )

assume p in Ball (z,r) ; :: thesis: p in ].(x - r),(x + r).[
then consider y being Point of RNS_Real such that
A2: ( p = y & ||.(z - y).|| < r ) ;
reconsider u = y as Real ;
A3: u - x = y - z by A1, DUALSP03:4;
||.(y - z).|| < r by A2, NORMSP_1:7;
then |.(u - x).| < r by A3, EUCLID:def 2;
hence p in ].(x - r),(x + r).[ by A2, RCOMP_1:1; :: thesis: verum

end;

assume A4: p in ].(x - r),(x + r).[ ; :: thesis: p in Ball (z,r)
then reconsider u = p as Real ;
A5: |.(u - x).| < r by A4, RCOMP_1:1;
reconsider y = u as Point of RNS_Real by XREAL_0:def 1;
u - x = y - z by A1, DUALSP03:4;
then ||.(y - z).|| < r by A5, EUCLID:def 2;
then ||.(z - y).|| < r by NORMSP_1:7;
hence p in Ball (z,r) ; :: thesis: verum

end;

hence Ball (z,r) = ].(x - r),(x + r).[ by TARSKI:2; :: thesis: verum