let a, b, r be Real; :: 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, Th13;
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, Th18;
reconsider br = b - r as negative Real by A4, XREAL_1:49;
set y = br / 2;
reconsider r = r as positive Real by A1;
|[a,(br / 2)]| - |[a,b]| = |[(a - a),((br / 2) - b)]| by EUCLID:62;
then A5: |.(|[a,(br / 2)]| - |[a,b]|).| = |.((br / 2) - b).| by TOPREAL6:23
.= |.(b - (br / 2)).| by COMPLEX1:60
.= (b + r) / 2 by ABSVALUE:def 1 ;
b + r < r + r by A4, XREAL_1:6;
then (b + r) / 2 < (r + r) / 2 by XREAL_1:74;
then |[a,(br / 2)]| in Ball (|[a,b]|,r) by A5, TOPREAL9:7;
hence contradiction by A3, Th18; :: thesis: verum

end;

assume A6: r <= b ; :: thesis: Ball (|[a,b]|,r) c= y>=0-plane
let x be object ; :: 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:52;
A10: |[((z `1) - a),((z `2) - b)]| `2 = (z `2) - b by EUCLID:52;
A11: z = |[(z `1),(z `2)]| by EUCLID:53;
then z - |[a,b]| = |[((z `1) - a),((z `2) - b)]| by EUCLID:62;
then |.(z - |[a,b]|).| = sqrt ((((z `1) - a) ^2) + (((z `2) - b) ^2)) by A9, A10, JGRAPH_1:30;
then |.((z `2) - b).| <= |.(z - |[a,b]|).| by COMPLEX1:79;
then |.((z `2) - b).| < r by A8, XXREAL_0:2;
then A12: |.(b - (z `2)).| < r by COMPLEX1:60;

now :: thesis: not z `2 < 0

assume z `2 < 0 ; :: thesis: contradiction
then b - (z `2) > b by XREAL_1:46;
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