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 } )
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 } ;
A1: { 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
A2: ( u = q & |.(|[0 ,0 ]| - q).| < r ) ;
|.(|[0 ,0 ]| - q).| = |.(q - |[0 ,0 ]|).| by TOPRNS_1:28
.= |.q.| by EUCLID:58, RLVECT_1:26 ;
hence u in { q where q is Point of (TOP-REAL 2) : |.q.| < r } by A2; :: thesis: verum

end;

A3: { 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
A4: ( u = q & |.q.| < r ) ;
|.(|[0 ,0 ]| - q).| = |.(q - |[0 ,0 ]|).| by TOPRNS_1:28
.= |.q.| by EUCLID:58, RLVECT_1:26 ;
hence u in { q where q is Point of (TOP-REAL 2) : |.(|[0 ,0 ]| - q).| < r } by A4; :: thesis: verum

end;

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