let u be Point of RealSpace; :: thesis: for r, u1 being Real st u1 = u holds
Ball (u,r) = { s where s is Real : ( u1 - r < s & s < u1 + r ) }
let r, u1 be Real; :: thesis: ( u1 = u implies Ball (u,r) = { s where s is Real : ( u1 - r < s & s < u1 + r ) } )
assume A1: u1 = u ; :: thesis: Ball (u,r) = { s where s is Real : ( u1 - r < s & s < u1 + r ) }
{ s where s is Real : ( u1 - r < s & s < u1 + r ) } = { q where q is Element of RealSpace : dist (u,q) < r }

proof

A2: { q where q is Element of RealSpace : dist (u,q) < r } c= { s where s is Real : ( u1 - r < s & s < u1 + r ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Element of RealSpace : dist (u,q) < r } or x in { s where s is Real : ( u1 - r < s & s < u1 + r ) } )
assume x in { q where q is Element of RealSpace : dist (u,q) < r } ; :: thesis: x in { s where s is Real : ( u1 - r < s & s < u1 + r ) }
then consider q being Element of RealSpace such that
A3: x = q and
A4: dist (u,q) < r ;
reconsider s1 = q as Real ;
A5: |.(u1 - s1).| < r by A1, A4, TOPMETR:11;
then u1 - s1 < r by SEQ_2:1;
then (u1 - s1) + s1 < r + s1 by XREAL_1:6;
then A6: u1 - r < (r + s1) - r by XREAL_1:9;
- r < u1 - s1 by A5, SEQ_2:1;
then (- r) + s1 < (u1 - s1) + s1 by XREAL_1:6;
then (s1 - r) + r < u1 + r by XREAL_1:6;
hence x in { s where s is Real : ( u1 - r < s & s < u1 + r ) } by A3, A6; :: thesis: verum

end;

{ s where s is Real : ( u1 - r < s & s < u1 + r ) } c= { q where q is Element of RealSpace : dist (u,q) < r }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { s where s is Real : ( u1 - r < s & s < u1 + r ) } or x in { q where q is Element of RealSpace : dist (u,q) < r } )
assume x in { s where s is Real : ( u1 - r < s & s < u1 + r ) } ; :: thesis: x in { q where q is Element of RealSpace : dist (u,q) < r }
then consider s being Real such that
A7: x = s and
A8: u1 - r < s and
A9: s < u1 + r ;
s in REAL by XREAL_0:def 1;
then reconsider q1 = s as Point of RealSpace by METRIC_1:def 13;
s - r < (u1 + r) - r by A9, XREAL_1:9;
then A10: (s + (- r)) - s < u1 - s by XREAL_1:9;
(u1 - r) + r < s + r by A8, XREAL_1:6;
then u1 - s < (s + r) - s by XREAL_1:9;
then |.(u1 - s).| < r by A10, SEQ_2:1;
then dist (u,q1) < r by A1, TOPMETR:11;
hence x in { q where q is Element of RealSpace : dist (u,q) < r } by A7; :: thesis: verum

end;

hence { s where s is Real : ( u1 - r < s & s < u1 + r ) } = { q where q is Element of RealSpace : dist (u,q) < r } by A2, XBOOLE_0:def 10; :: thesis: verum

end;

hence Ball (u,r) = { s where s is Real : ( u1 - r < s & s < u1 + r ) } by METRIC_1:17; :: thesis: verum