let r be Real; for p being Point of (TOP-REAL 3)
for e being Point of (Euclid 3) st p = e & p `3 = 0 holds
product ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) c= Ball (e,r)
let p be Point of (TOP-REAL 3); for e being Point of (Euclid 3) st p = e & p `3 = 0 holds
product ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) c= Ball (e,r)
let e be Point of (Euclid 3); ( p = e & p `3 = 0 implies product ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) c= Ball (e,r) )
set A = ].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[;
set B = ].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[;
set C = {0};
set f = (1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0});
assume that
A1:
p = e
and
A2:
p `3 = 0
; product ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) c= Ball (e,r)
let a be object ; TARSKI:def 3 ( not a in product ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) or a in Ball (e,r) )
assume
a in product ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0}))
; a in Ball (e,r)
then consider g being Function such that
A3:
a = g
and
A4:
dom g = dom ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0}))
and
A5:
for x being object st x in dom ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) holds
g . x in ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) . x
by CARD_3:def 5;
A6:
].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[ = { m where m is Real : ( (p `1) - (r / (sqrt 2)) < m & m < (p `1) + (r / (sqrt 2)) ) }
by RCOMP_1:def 2;
A7:
].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[ = { n where n is Real : ( (p `2) - (r / (sqrt 2)) < n & n < (p `2) + (r / (sqrt 2)) ) }
by RCOMP_1:def 2;
A8:
dom ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) = {1,2,3}
by FUNCT_4:128;
then A9:
( 1 in dom ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) & 2 in dom ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) & 3 in dom ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) )
by ENUMSET1:def 1;
A10:
( ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) . 1 = ].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[ & ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) . 2 = ].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[ & ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) . 3 = {0} )
by FUNCT_4:135, FUNCT_4:134;
then A11:
( g . 1 in ].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[ & g . 2 in ].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[ & g . 3 in {0} )
by A5, A9;
then consider m being Real such that
A12:
m = g . 1
and
( (p `1) - (r / (sqrt 2)) < m & m < (p `1) + (r / (sqrt 2)) )
by A6;
consider n being Real such that
A13:
n = g . 2
and
( (p `2) - (r / (sqrt 2)) < n & n < (p `2) + (r / (sqrt 2)) )
by A7, A11;
g . 3 in ((1,2,3) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[,{0})) . 3
by A5, A9;
then A14:
g . 3 = 0
by A10, TARSKI:def 1;
(p `1) + (r / (sqrt 2)) > (p `1) - (r / (sqrt 2))
by A11, XXREAL_1:28;
then
(p `1) - ((p `1) + (r / (sqrt 2))) < (p `1) - ((p `1) - (r / (sqrt 2)))
by XREAL_1:10;
then
(- (r / (sqrt 2))) + (r / (sqrt 2)) < (r / (sqrt 2)) + (r / (sqrt 2))
by XREAL_1:6;
then A15:
0 < r
;
A16: dom <*(g . 1),(g . 2),(g . 3)*> =
Seg (len <*(g . 1),(g . 2),(g . 3)*>)
by FINSEQ_1:def 3
.=
{1,2,3}
by FINSEQ_1:45, FINSEQ_3:1
;
then A17:
a = |[m,n,0]|
by A3, A4, A12, A13, A16, A14, FUNCT_4:128, FUNCT_1:2;
then reconsider c = a as Point of (TOP-REAL 3) ;
reconsider b = c as Point of (Euclid 3) by TOPREAL3:8;
( |.(m - (p `1)).| < r / (sqrt 2) & |.(n - (p `2)).| < r / (sqrt 2) )
by A11, A12, A13, RCOMP_1:1;
then
( |.(m - (p `1)).| ^2 < (r / (sqrt 2)) ^2 & |.(n - (p `2)).| ^2 < (r / (sqrt 2)) ^2 )
by SQUARE_1:16;
then
( |.(m - (p `1)).| ^2 < (r ^2) / ((sqrt 2) ^2) & |.(n - (p `2)).| ^2 < (r ^2) / ((sqrt 2) ^2) )
by XCMPLX_1:76;
then
( |.(m - (p `1)).| ^2 < (r ^2) / 2 & |.(n - (p `2)).| ^2 < (r ^2) / 2 )
by SQUARE_1:def 2;
then
( (m - (p `1)) ^2 < (r ^2) / 2 & (n - (p `2)) ^2 < (r ^2) / 2 )
by COMPLEX1:75;
then
((m - (p `1)) ^2) + ((n - (p `2)) ^2) < ((r ^2) / 2) + ((r ^2) / 2)
by XREAL_1:8;
then
sqrt (((m - (p `1)) ^2) + ((n - (p `2)) ^2)) < sqrt (r ^2)
by SQUARE_1:27;
then A18:
sqrt (((m - (p `1)) ^2) + ((n - (p `2)) ^2)) < r
by A15, SQUARE_1:22;
A19:
( m = c `1 & n = c `2 )
by A17, EUCLID_5:2;
dist (b,e) =
(Pitag_dist 3) . (b,e)
by METRIC_1:def 1
.=
sqrt (((((c `1) - (p `1)) ^2) + (((c `2) - (p `2)) ^2)) + (((c `3) - (p `3)) ^2))
by A1, Th37
.=
sqrt (((((c `1) - (p `1)) ^2) + (((c `2) - (p `2)) ^2)) + ((Q - Q) ^2))
by A2, A17, EUCLID_5:2
.=
sqrt (((((c `1) - (p `1)) ^2) + (((c `2) - (p `2)) ^2)) + Q)
;
hence
a in Ball (e,r)
by A18, A19, METRIC_1:11; verum