let a, b, r be real number ; :: thesis: ( r > 0 & b >= 0 implies ( Ball |[a,b]|,r misses y=0-line iff r <= b ) )
assume A1: ( r > 0 & b >= 0 ) ; :: thesis: ( Ball |[a,b]|,r misses y=0-line iff r <= b )

hereby :: thesis: ( r <= b implies Ball |[a,b]|,r misses y=0-line )

assume that
A2: Ball |[a,b]|,r misses y=0-line and
A3: r > b ; :: thesis: contradiction
( |[a,0 ]| - |[a,b]| = |[(a - a),(0 - b)]| & 0 - b is Real ) by EUCLID:66;
then |.(|[a,0 ]| - |[a,b]|).| = |.(0 - b).| by TOPREAL6:31
.= |.(b - 0 ).| by COMPLEX1:146 ;
then |.(|[a,0 ]| - |[a,b]|).| < r by A1, A3, ABSVALUE:def 1;
then ( |[a,0 ]| in Ball |[a,b]|,r & |[a,0 ]| in y=0-line ) by Th19, TOPREAL9:7;
hence contradiction by A2, XBOOLE_0:3; :: thesis: verum

end;

assume A4: r <= b ; :: thesis: Ball |[a,b]|,r misses y=0-line
assume Ball |[a,b]|,r meets y=0-line ; :: thesis: contradiction
then consider x being set such that
A5: ( x in Ball |[a,b]|,r & x in y=0-line ) by XBOOLE_0:3;
reconsider x = x as Element of (TOP-REAL 2) by A5;
A6: x = |[(x `1 ),(x `2 )]| by EUCLID:57;
then x `2 = 0 by A5, Th19;
then x - |[a,b]| = |[((x `1 ) - a),(0 - b)]| by A6, EUCLID:66;
then ( (x - |[a,b]|) `1 = (x `1 ) - a & (x - |[a,b]|) `2 = 0 - b ) by EUCLID:56;
then ( (x `1 ) - a is Real & 0 - b is Real & |.(x - |[a,b]|).| = sqrt ((((x `1 ) - a) ^2 ) + ((0 - b) ^2 )) ) by JGRAPH_1:47;
then |.(x - |[a,b]|).| >= abs (0 - b) by COMPLEX1:165;
then ( |.(x - |[a,b]|).| >= abs (b - 0 ) & |.(x - |[a,b]|).| < r ) by A5, COMPLEX1:146, TOPREAL9:7;
then abs b < r by XXREAL_0:2;
hence contradiction by A1, A4, ABSVALUE:def 1; :: thesis: verum