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:41;
then consider w being rational number such that
A1: ( x < w & w < x + (r / 2) ) by RAT_1:22;
y < y + (r / 2) by XREAL_1:41;
then consider v being rational number such that
A2: ( y < v & v < y + (r / 2) ) by RAT_1:22;
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]| )
( w - x is Real & v - y is Real & |[w,v]| - |[x,v]| = |[(w - x),(v - v)]| & |[x,v]| - |[x,y]| = |[(x - x),(v - y)]| ) by EUCLID:66, XREAL_0:def 1;
then ( |.(|[w,v]| - |[x,v]|).| = abs (w - x) & |.(|[x,v]| - |[x,y]|).| = |.(v - y).| & w - x > 0 & v - y > 0 ) by A1, A2, TOPREAL6:31, XREAL_1:52;
then ( |.(|[w,v]| - |[x,v]|).| = w - x & |.(|[x,v]| - |[x,y]|).| = v - y ) by ABSVALUE:def 1;
then ( |.(|[w,v]| - |[x,v]|).| < (x + (r / 2)) - x & |.(|[x,v]| - |[x,y]|).| <= (y + (r / 2)) - y ) by A1, A2, XREAL_1:11;
then ( |.(|[w,v]| - |[x,y]|).| <= |.(|[w,v]| - |[x,v]|).| + |.(|[x,v]| - |[x,y]|).| & |.(|[w,v]| - |[x,v]|).| + |.(|[x,v]| - |[x,y]|).| < ((x + (r / 2)) - x) + ((y + (r / 2)) - y) ) by TOPRNS_1:35, XREAL_1:10;
then |.(|[w,v]| - |[x,y]|).| < r by 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 A2, SPPOL_2:1; :: thesis: verum