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 object ; :: 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:27
.= |.q.| by EUCLID:54, RLVECT_1:13 ;
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 object ; :: 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:27
.= |.q.| by EUCLID:54, RLVECT_1:13 ;
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:2
.= { q where q is Point of (TOP-REAL 2) : |.q.| < r } by A1, A3 ;
:: thesis: verum