let x be Point of RealSpace; :: thesis: for r being Real holds Ball (x,r) = ].(x - r),(x + r).[

let r be Real; :: thesis: Ball (x,r) = ].(x - r),(x + r).[

reconsider x2 = x as Element of REAL by METRIC_1:def 13;

thus Ball (x,r) c= ].(x - r),(x + r).[ :: according to XBOOLE_0:def 10 :: thesis: ].(x - r),(x + r).[ c= Ball (x,r)

assume A3: y in ].(x - r),(x + r).[ ; :: thesis: y in Ball (x,r)

then reconsider y2 = y as Element of REAL ;

reconsider x1 = x, y1 = y2 as Element of RealSpace by METRIC_1:def 13;

|.(y2 - x).| = |.(- (y2 - x)).| by COMPLEX1:52

.= |.(x - y2).|

.= real_dist . (x2,y2) by METRIC_1:def 12 ;

then A4: real_dist . (x2,y2) < r by A3, RCOMP_1:1;

dist (x1,y1) = real_dist . (x2,y2) by METRIC_1:def 1, METRIC_1:def 13;

hence y in Ball (x,r) by A4, METRIC_1:11; :: thesis: verum

let r be Real; :: thesis: Ball (x,r) = ].(x - r),(x + r).[

reconsider x2 = x as Element of REAL by METRIC_1:def 13;

thus Ball (x,r) c= ].(x - r),(x + r).[ :: according to XBOOLE_0:def 10 :: thesis: ].(x - r),(x + r).[ c= Ball (x,r)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in ].(x - r),(x + r).[ or y in Ball (x,r) )
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Ball (x,r) or y in ].(x - r),(x + r).[ )

assume A1: y in Ball (x,r) ; :: thesis: y in ].(x - r),(x + r).[

then reconsider y1 = y as Element of RealSpace ;

reconsider y2 = y1 as Element of REAL by METRIC_1:def 13;

A2: dist (x,y1) = real_dist . (x2,y2) by METRIC_1:def 1, METRIC_1:def 13

.= |.(x2 - y2).| by METRIC_1:def 12

.= |.(- (y2 - x2)).|

.= |.(y2 - x2).| by COMPLEX1:52 ;

dist (x,y1) < r by A1, METRIC_1:11;

hence y in ].(x - r),(x + r).[ by A2, RCOMP_1:1; :: thesis: verum

end;assume A1: y in Ball (x,r) ; :: thesis: y in ].(x - r),(x + r).[

then reconsider y1 = y as Element of RealSpace ;

reconsider y2 = y1 as Element of REAL by METRIC_1:def 13;

A2: dist (x,y1) = real_dist . (x2,y2) by METRIC_1:def 1, METRIC_1:def 13

.= |.(x2 - y2).| by METRIC_1:def 12

.= |.(- (y2 - x2)).|

.= |.(y2 - x2).| by COMPLEX1:52 ;

dist (x,y1) < r by A1, METRIC_1:11;

hence y in ].(x - r),(x + r).[ by A2, RCOMP_1:1; :: thesis: verum

assume A3: y in ].(x - r),(x + r).[ ; :: thesis: y in Ball (x,r)

then reconsider y2 = y as Element of REAL ;

reconsider x1 = x, y1 = y2 as Element of RealSpace by METRIC_1:def 13;

|.(y2 - x).| = |.(- (y2 - x)).| by COMPLEX1:52

.= |.(x - y2).|

.= real_dist . (x2,y2) by METRIC_1:def 12 ;

then A4: real_dist . (x2,y2) < r by A3, RCOMP_1:1;

dist (x1,y1) = real_dist . (x2,y2) by METRIC_1:def 1, METRIC_1:def 13;

hence y in Ball (x,r) by A4, METRIC_1:11; :: thesis: verum