let u be Point of (Euclid 1); :: thesis: for r, u1 being real number st <*u1*> = u & r > 0 holds
Ball u,r = { <*s*> where s is Real : ( u1 - r < s & s < u1 + r ) }
let r, u1 be real number ; :: thesis: ( <*u1*> = u & r > 0 implies Ball u,r = { <*s*> where s is Real : ( u1 - r < s & s < u1 + r ) } )
assume A1: ( <*u1*> = u & r > 0 ) ; :: thesis: Ball u,r = { <*s*> where s is Real : ( u1 - r < s & s < u1 + r ) }
reconsider u1 = u1 as Real by XREAL_0:def 1;
{ <*s*> where s is Real : ( u1 - r < s & s < u1 + r ) } = { q where q is Element of (Euclid 1) : dist u,q < r }

proof

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

proof

let x be set ; :: 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 (Euclid 1) : 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 (Euclid 1) : dist u,q < r }
then consider s being Real such that
A3: ( x = <*s*> & u1 - r < s & s < u1 + r ) ;
reconsider q1 = <*s*> as Element of (Euclid 1) by FINSEQ_2:118;
(u1 - r) + r < s + r by A3, XREAL_1:8;
then A4: u1 - s < (s + r) - s by XREAL_1:11;
s - r < (u1 + r) - r by A3, XREAL_1:11;
then (s + (- r)) - s < u1 - s by XREAL_1:11;
then A5: abs (u1 - s) < r by A4, SEQ_2:9;
<*u1*> - <*s*> = <*(u1 - s)*> by RVSUM_1:50;
then sqr (<*u1*> - <*s*>) = <*((u1 - s) ^2 )*> by RVSUM_1:81;
then Sum (sqr (<*u1*> - <*s*>)) = (u1 - s) ^2 by FINSOP_1:12;
then A6: |.(<*u1*> - <*s*>).| < r by A5, COMPLEX1:158;
reconsider eu1 = <*u1*> as Element of REAL 1 by FINSEQ_2:118;
reconsider es = <*s*> as Element of REAL 1 by FINSEQ_2:118;
A7: the distance of (Euclid 1) . u,q1 = dist u,q1 by METRIC_1:def 1;
(Pitag_dist 1) . eu1,es < r by A6, EUCLID:def 6;
hence x in { q where q is Element of (Euclid 1) : dist u,q < r } by A1, A3, A7; :: thesis: verum

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Element of (Euclid 1) : 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 (Euclid 1) : dist u,q < r } ; :: thesis: x in { <*s*> where s is Real : ( u1 - r < s & s < u1 + r ) }
then consider q being Element of (Euclid 1) such that
A8: ( x = q & dist u,q < r ) ;
consider s1 being Real such that
A9: q = <*s1*> by FINSEQ_2:117;
reconsider eu = u, eq = q as Element of REAL 1 ;
(Pitag_dist 1) . eu,eq < r by A8, METRIC_1:def 1;
then A10: |.(<*u1*> - <*s1*>).| < r by A1, A9, EUCLID:def 6;
<*u1*> - <*s1*> = <*(u1 - s1)*> by RVSUM_1:50;
then sqr (<*u1*> - <*s1*>) = <*((u1 - s1) ^2 )*> by RVSUM_1:81;
then Sum (sqr (<*u1*> - <*s1*>)) = (u1 - s1) ^2 by FINSOP_1:12;
then sqrt (Sum (sqr (<*u1*> - <*s1*>))) = abs (u1 - s1) by COMPLEX1:158;
then A11: ( - r < u1 - s1 & u1 - s1 < r ) by A10, SEQ_2:9;
then (- r) + s1 < (u1 - s1) + s1 by XREAL_1:8;
then A12: (s1 - r) + r < u1 + r by XREAL_1:8;
(u1 - s1) + s1 < r + s1 by A11, XREAL_1:8;
then u1 - r < (r + s1) - r by XREAL_1:11;
hence x in { <*s*> where s is Real : ( u1 - r < s & s < u1 + r ) } by A8, A9, A12; :: thesis: verum

end;

hence { <*s*> where s is Real : ( u1 - r < s & s < u1 + r ) } = { q where q is Element of (Euclid 1) : 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:18; :: thesis: verum