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 that
A1: r > 0 and
A2: 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 )

A3: |[a,0 ]| in y=0-line by Th19;
assume that
A4: Ball |[a,b]|,r misses y=0-line and
A5: r > b ; :: thesis: contradiction
|[a,0 ]| - |[a,b]| = |[(a - a),(0 - b)]| 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 A2, A5, ABSVALUE:def 1;
then |[a,0 ]| in Ball |[a,b]|,r by TOPREAL9:7;
hence contradiction by A3, A4, XBOOLE_0:3; :: thesis: verum

end;

assume A6: 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
A7: x in Ball |[a,b]|,r and
A8: x in y=0-line by XBOOLE_0:3;
reconsider x = x as Element of (TOP-REAL 2) by A7;
A9: x = |[(x `1 ),(x `2 )]| by EUCLID:57;
then x `2 = 0 by A8, Th19;
then A10: x - |[a,b]| = |[((x `1 ) - a),(0 - b)]| by A9, EUCLID:66;
then A11: (x - |[a,b]|) `2 = 0 - b by EUCLID:56;
(x - |[a,b]|) `1 = (x `1 ) - a by A10, EUCLID:56;
then |.(x - |[a,b]|).| = sqrt ((((x `1 ) - a) ^2 ) + ((0 - b) ^2 )) by A11, JGRAPH_1:47;
then |.(x - |[a,b]|).| >= abs (0 - b) by COMPLEX1:165;
then A12: |.(x - |[a,b]|).| >= abs (b - 0 ) by COMPLEX1:146;
|.(x - |[a,b]|).| < r by A7, TOPREAL9:7;
then abs b < r by A12, XXREAL_0:2;
hence contradiction by A1, A6, ABSVALUE:def 1; :: thesis: verum