let x, y be Real; :: thesis: for r being positive Real ex w, v being Rational st
( |[w,v]| in Ball (|[x,y]|,r) & |[w,v]| <> |[x,y]| )
let r be positive Real; :: thesis: ex w, v being Rational st
( |[w,v]| in Ball (|[x,y]|,r) & |[w,v]| <> |[x,y]| )
x < x + (r / 2) by XREAL_1:39;
then consider w being Rational such that
A1: x < w and
A2: w < x + (r / 2) by RAT_1:7;
A3: w - x > 0 by A1, XREAL_1:50;
y < y + (r / 2) by XREAL_1:39;
then consider v being Rational such that
A4: y < v and
A5: v < y + (r / 2) by RAT_1:7;
A6: v - y > 0 by A4, XREAL_1:50;
|[w,v]| - |[x,v]| = |[(w - x),(v - v)]| by EUCLID:62;
then |.(|[w,v]| - |[x,v]|).| = |.(w - x).| by TOPREAL6:23;
then |.(|[w,v]| - |[x,v]|).| = w - x by A3, ABSVALUE:def 1;
then A7: |.(|[w,v]| - |[x,v]|).| < (x + (r / 2)) - x by A2, XREAL_1:9;
take w ; :: thesis: ex v being Rational st
( |[w,v]| in Ball (|[x,y]|,r) & |[w,v]| <> |[x,y]| )
take v ; :: thesis: ( |[w,v]| in Ball (|[x,y]|,r) & |[w,v]| <> |[x,y]| )
A8: |[x,v]| - |[x,y]| = |[(x - x),(v - y)]| by EUCLID:62;
A9: |.(|[w,v]| - |[x,y]|).| <= |.(|[w,v]| - |[x,v]|).| + |.(|[x,v]| - |[x,y]|).| by TOPRNS_1:34;
|.(|[x,v]| - |[x,y]|).| = |.(v - y).| by A8, TOPREAL6:23;
then |.(|[x,v]| - |[x,y]|).| = v - y by A6, ABSVALUE:def 1;
then |.(|[x,v]| - |[x,y]|).| <= (y + (r / 2)) - y by A5, XREAL_1:9;
then |.(|[w,v]| - |[x,v]|).| + |.(|[x,v]| - |[x,y]|).| < ((x + (r / 2)) - x) + ((y + (r / 2)) - y) by A7, XREAL_1:8;
then |.(|[w,v]| - |[x,y]|).| < r by A9, XXREAL_0:2;
hence |[w,v]| in Ball (|[x,y]|,r) by TOPREAL9:7; :: thesis: |[w,v]| <> |[x,y]|
thus |[w,v]| <> |[x,y]| by A4, SPPOL_2:1; :: thesis: verum