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

hereby :: thesis: ( r <= b implies Ball |[a,b]|,r c= y>=0-plane )

A2: |[a,b]| in Ball |[a,b]|,r by A1, Th17;
assume that
A3: Ball |[a,b]|,r c= y>=0-plane and
A4: r > b ; :: thesis: contradiction
reconsider b = b as non negative Real by A2, A3, Th22, XREAL_0:def 1;
reconsider br = b - r as negative Real by A4, XREAL_1:51;
set y = br / 2;
reconsider r = r as positive Real by A1, XREAL_0:def 1;
|[a,(br / 2)]| - |[a,b]| = |[(a - a),((br / 2) - b)]| by EUCLID:66;
then A5: |.(|[a,(br / 2)]| - |[a,b]|).| = |.((br / 2) - b).| by TOPREAL6:31
.= |.(b - (br / 2)).| by COMPLEX1:146
.= (b + r) / 2 by ABSVALUE:def 1 ;
b + r < r + r by A4, XREAL_1:8;
then (b + r) / 2 < (r + r) / 2 by XREAL_1:76;
then |[a,(br / 2)]| in Ball |[a,b]|,r by A5, TOPREAL9:7;
hence contradiction by A3, Th22; :: thesis: verum

end;

assume A6: r <= b ; :: thesis: Ball |[a,b]|,r c= y>=0-plane
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Ball |[a,b]|,r or x in y>=0-plane )
assume A7: x in Ball |[a,b]|,r ; :: thesis: x in y>=0-plane
then reconsider z = x as Element of (TOP-REAL 2) ;
A8: |.(z - |[a,b]|).| < r by A7, TOPREAL9:7;
A9: |[((z `1 ) - a),((z `2 ) - b)]| `1 = (z `1 ) - a by EUCLID:56;
A10: |[((z `1 ) - a),((z `2 ) - b)]| `2 = (z `2 ) - b by EUCLID:56;
A11: z = |[(z `1 ),(z `2 )]| by EUCLID:57;
then z - |[a,b]| = |[((z `1 ) - a),((z `2 ) - b)]| by EUCLID:66;
then |.(z - |[a,b]|).| = sqrt ((((z `1 ) - a) ^2 ) + (((z `2 ) - b) ^2 )) by A9, A10, JGRAPH_1:47;
then abs ((z `2 ) - b) <= |.(z - |[a,b]|).| by COMPLEX1:165;
then abs ((z `2 ) - b) < r by A8, XXREAL_0:2;
then A12: abs (b - (z `2 )) < r by COMPLEX1:146;

now

assume z `2 < 0 ; :: thesis: contradiction
then b - (z `2 ) > b by XREAL_1:48;
then b - (z `2 ) > r by A6, XXREAL_0:2;
hence contradiction by A1, A12, ABSVALUE:def 1; :: thesis: verum

end;

hence x in y>=0-plane by A11; :: thesis: verum