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