let u be Point of (Euclid 1); :: thesis: for r, u1 being Real st <*u1*> = u holds

cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) }

let r, u1 be Real; :: thesis: ( <*u1*> = u implies cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } )

assume A1: <*u1*> = u ; :: thesis: cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) }

set E1 = { q where q is Element of (Euclid 1) : dist (u,q) <= r } ;

reconsider u1 = u1 as Element of REAL by XREAL_0:def 1;

set R1 = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } ;

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

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

cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) }

let r, u1 be Real; :: thesis: ( <*u1*> = u implies cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } )

assume A1: <*u1*> = u ; :: thesis: cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) }

set E1 = { q where q is Element of (Euclid 1) : dist (u,q) <= r } ;

reconsider u1 = u1 as Element of REAL by XREAL_0:def 1;

set R1 = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } ;

A2: { 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

{ <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } c= { q where q is Element of (Euclid 1) : dist (u,q) <= r }
let x be object ; :: 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

A3: x = q and

A4: dist (u,q) <= r ;

q is Tuple of 1, REAL by FINSEQ_2:131;

then consider s1 being Element of REAL such that

A5: q = <*s1*> by FINSEQ_2:97;

<*u1*> - <*s1*> = <*(u1 - s1)*> by RVSUM_1:29;

then sqr (<*u1*> - <*s1*>) = <*((u1 - s1) ^2)*> by RVSUM_1:55;

then Sum (sqr (<*u1*> - <*s1*>)) = (u1 - s1) ^2 by RVSUM_1:73;

then A6: sqrt (Sum (sqr (<*u1*> - <*s1*>))) = |.(u1 - s1).| by COMPLEX1:72;

A7: |.(<*u1*> - <*s1*>).| <= r by A1, A4, A5, EUCLID:def 6;

then u1 - s1 <= r by A6, ABSVALUE:5;

then (u1 - s1) + s1 <= r + s1 by XREAL_1:6;

then A8: u1 - r <= (r + s1) - r by XREAL_1:9;

- r <= u1 - s1 by A6, A7, ABSVALUE:5;

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, A5, A8; :: thesis: verum

end;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

A3: x = q and

A4: dist (u,q) <= r ;

q is Tuple of 1, REAL by FINSEQ_2:131;

then consider s1 being Element of REAL such that

A5: q = <*s1*> by FINSEQ_2:97;

<*u1*> - <*s1*> = <*(u1 - s1)*> by RVSUM_1:29;

then sqr (<*u1*> - <*s1*>) = <*((u1 - s1) ^2)*> by RVSUM_1:55;

then Sum (sqr (<*u1*> - <*s1*>)) = (u1 - s1) ^2 by RVSUM_1:73;

then A6: sqrt (Sum (sqr (<*u1*> - <*s1*>))) = |.(u1 - s1).| by COMPLEX1:72;

A7: |.(<*u1*> - <*s1*>).| <= r by A1, A4, A5, EUCLID:def 6;

then u1 - s1 <= r by A6, ABSVALUE:5;

then (u1 - s1) + s1 <= r + s1 by XREAL_1:6;

then A8: u1 - r <= (r + s1) - r by XREAL_1:9;

- r <= u1 - s1 by A6, A7, ABSVALUE:5;

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, A5, A8; :: thesis: verum

proof

then
{ q where q is Element of (Euclid 1) : dist (u,q) <= r } = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) }
by A2;
reconsider eu1 = <*u1*> as Element of REAL 1 by FINSEQ_2:98;

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 (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

A9: x = <*s*> and

A10: u1 - r <= s and

A11: s <= u1 + r ;

s - r <= (u1 + r) - r by A11, XREAL_1:9;

then A12: (s + (- r)) - s <= u1 - s by XREAL_1:9;

reconsider s = s as Element of REAL by XREAL_0:def 1;

reconsider es = <*s*> as Element of REAL 1 by FINSEQ_2:98;

reconsider q1 = <*s*> as Element of (Euclid 1) by FINSEQ_2:98;

<*u1*> - <*s*> = <*(u1 - s)*> by RVSUM_1:29;

then sqr (<*u1*> - <*s*>) = <*((u1 - s) ^2)*> by RVSUM_1:55;

then A13: Sum (sqr (<*u1*> - <*s*>)) = (u1 - s) ^2 by RVSUM_1:73;

(u1 - r) + r <= s + r by A10, XREAL_1:6;

then u1 - s <= (s + r) - s by XREAL_1:9;

then |.(u1 - s).| <= r by A12, ABSVALUE:5;

then |.(<*u1*> - <*s*>).| <= r by A13, COMPLEX1:72;

then ( the distance of (Euclid 1) . (u,q1) = dist (u,q1) & (Pitag_dist 1) . (eu1,es) <= r ) by EUCLID:def 6;

hence x in { q where q is Element of (Euclid 1) : dist (u,q) <= r } by A1, A9; :: thesis: verum

end;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 (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

A9: x = <*s*> and

A10: u1 - r <= s and

A11: s <= u1 + r ;

s - r <= (u1 + r) - r by A11, XREAL_1:9;

then A12: (s + (- r)) - s <= u1 - s by XREAL_1:9;

reconsider s = s as Element of REAL by XREAL_0:def 1;

reconsider es = <*s*> as Element of REAL 1 by FINSEQ_2:98;

reconsider q1 = <*s*> as Element of (Euclid 1) by FINSEQ_2:98;

<*u1*> - <*s*> = <*(u1 - s)*> by RVSUM_1:29;

then sqr (<*u1*> - <*s*>) = <*((u1 - s) ^2)*> by RVSUM_1:55;

then A13: Sum (sqr (<*u1*> - <*s*>)) = (u1 - s) ^2 by RVSUM_1:73;

(u1 - r) + r <= s + r by A10, XREAL_1:6;

then u1 - s <= (s + r) - s by XREAL_1:9;

then |.(u1 - s).| <= r by A12, ABSVALUE:5;

then |.(<*u1*> - <*s*>).| <= r by A13, COMPLEX1:72;

then ( the distance of (Euclid 1) . (u,q1) = dist (u,q1) & (Pitag_dist 1) . (eu1,es) <= r ) by EUCLID:def 6;

hence x in { q where q is Element of (Euclid 1) : dist (u,q) <= r } by A1, A9; :: thesis: verum

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