let r be Real; :: thesis: for y being Point of (Euclid 2) st y = |[0 ,0 ]| holds
Ball y,r = { q where q is Point of (TOP-REAL 2) : |.q.| < r }
let y be Point of (Euclid 2); :: thesis: ( y = |[0 ,0 ]| implies Ball y,r = { q where q is Point of (TOP-REAL 2) : |.q.| < r } )
assume A1: y = |[0 ,0 ]| ; :: thesis: Ball y,r = { q where q is Point of (TOP-REAL 2) : |.q.| < r }
set X = { q where q is Point of (TOP-REAL 2) : |.(|[0 ,0 ]| - q).| < r } ;
set Y = { q where q is Point of (TOP-REAL 2) : |.q.| < r } ;
A2: { q where q is Point of (TOP-REAL 2) : |.(|[0 ,0 ]| - q).| < r } c= { q where q is Point of (TOP-REAL 2) : |.q.| < r }

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in { q where q is Point of (TOP-REAL 2) : |.(|[0 ,0 ]| - q).| < r } or u in { q where q is Point of (TOP-REAL 2) : |.q.| < r } )
assume u in { q where q is Point of (TOP-REAL 2) : |.(|[0 ,0 ]| - q).| < r } ; :: thesis: u in { q where q is Point of (TOP-REAL 2) : |.q.| < r }
then consider q being Point of (TOP-REAL 2) such that
A3: ( u = q & |.(|[0 ,0 ]| - q).| < r ) ;
|.(|[0 ,0 ]| - q).| = |.(q - |[0 ,0 ]|).| by TOPRNS_1:28
.= |.q.| by EUCLID:58, RLVECT_1:26, RLVECT_1:27 ;
hence u in { q where q is Point of (TOP-REAL 2) : |.q.| < r } by A3; :: thesis: verum

end;

A4: { q where q is Point of (TOP-REAL 2) : |.q.| < r } c= { q where q is Point of (TOP-REAL 2) : |.(|[0 ,0 ]| - q).| < r }

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in { q where q is Point of (TOP-REAL 2) : |.q.| < r } or u in { q where q is Point of (TOP-REAL 2) : |.(|[0 ,0 ]| - q).| < r } )
assume u in { q where q is Point of (TOP-REAL 2) : |.q.| < r } ; :: thesis: u in { q where q is Point of (TOP-REAL 2) : |.(|[0 ,0 ]| - q).| < r }
then consider q being Point of (TOP-REAL 2) such that
A5: ( u = q & |.q.| < r ) ;
|.(|[0 ,0 ]| - q).| = |.(q - |[0 ,0 ]|).| by TOPRNS_1:28
.= |.q.| by EUCLID:58, RLVECT_1:26, RLVECT_1:27 ;
hence u in { q where q is Point of (TOP-REAL 2) : |.(|[0 ,0 ]| - q).| < r } by A5; :: thesis: verum

end;

thus Ball y,r = { q where q is Point of (TOP-REAL 2) : |.(|[0 ,0 ]| - q).| < r } by A1, JGRAPH_2:10
.= { q where q is Point of (TOP-REAL 2) : |.q.| < r } by A2, A4, XBOOLE_0:def 10 ; :: thesis: verum