let a, b, r be Real; :: 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 ;
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:62;
then |.(|[a,0]| - |[a,b]|).| = |.(0 - b).| by TOPREAL6:23
.= |.(b - 0).| by COMPLEX1:60 ;
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 object 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:53;
then x `2 = 0 by A8, Th15;
then A10: x - |[a,b]| = |[((x `1) - a),(0 - b)]| by A9, EUCLID:62;
then A11: (x - |[a,b]|) `2 = 0 - b by EUCLID:52;
(x - |[a,b]|) `1 = (x `1) - a by A10, EUCLID:52;
then |.(x - |[a,b]|).| = sqrt ((((x `1) - a) ^2) + ((0 - b) ^2)) by A11, JGRAPH_1:30;
then |.(x - |[a,b]|).| >= |.(0 - b).| by COMPLEX1:79;
then A12: |.(x - |[a,b]|).| >= |.(b - 0).| by COMPLEX1:60;
|.(x - |[a,b]|).| < r by A7, TOPREAL9:7;
then |.b.| < r by A12, XXREAL_0:2;
hence contradiction by A1, A6, ABSVALUE:def 1; :: thesis: verum