let a, b, r be Real; ( r > 0 implies ( Ball (|[a,b]|,r) c= y>=0-plane iff r <= b ) )
assume A1:
r > 0
; ( Ball (|[a,b]|,r) c= y>=0-plane iff r <= b )
hereby ( 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
;
contradictionreconsider 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;
verum
end;
assume A6:
r <= b
; Ball (|[a,b]|,r) c= y>=0-plane
let x be object ; TARSKI:def 3 ( not x in Ball (|[a,b]|,r) or x in y>=0-plane )
assume A7:
x in Ball (|[a,b]|,r)
; 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;
hence
x in y>=0-plane
by A11; verum