let x be Point of RealSpace ; :: thesis: for x9, r being Real st x9 = x holds
Ball x,r = ].(x9 - r),(x9 + r).[
let x9, r be Real; :: thesis: ( x9 = x implies Ball x,r = ].(x9 - r),(x9 + r).[ )
assume A1: x9 = x ; :: thesis: Ball x,r = ].(x9 - r),(x9 + r).[
thus Ball x,r c= ].(x9 - r),(x9 + r).[ :: according to XBOOLE_0:def 10 :: thesis: ].(x9 - r),(x9 + r).[ c= Ball x,r

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Ball x,r or y in ].(x9 - r),(x9 + r).[ )
assume A2: y in Ball x,r ; :: thesis: y in ].(x9 - r),(x9 + r).[
then reconsider y1 = y as Element of RealSpace ;
reconsider x2 = x, y2 = y1 as Element of REAL by METRIC_1:def 14;
A3: dist x,y1 = real_dist . x2,y2 by METRIC_1:def 1, METRIC_1:def 14
.= abs (x2 - y2) by METRIC_1:def 13
.= abs (- (y2 - x2))
.= abs (y2 - x2) by COMPLEX1:138 ;
dist x,y1 < r by A2, METRIC_1:12;
hence y in ].(x9 - r),(x9 + r).[ by A1, A3, RCOMP_1:8; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in ].(x9 - r),(x9 + r).[ or y in Ball x,r )
assume A4: y in ].(x9 - r),(x9 + r).[ ; :: thesis: y in Ball x,r
then reconsider y2 = y as Real ;
reconsider x1 = x9, y1 = y2 as Element of RealSpace by METRIC_1:def 14;
abs (y2 - x9) = abs (- (y2 - x9)) by COMPLEX1:138
.= abs (x9 - y2)
.= real_dist . x9,y2 by METRIC_1:def 13 ;
then A5: real_dist . x9,y2 < r by A4, RCOMP_1:8;
dist x1,y1 = real_dist . x9,y2 by METRIC_1:def 1, METRIC_1:def 14;
hence y in Ball x,r by A1, A5, METRIC_1:12; :: thesis: verum