let p be Point of (TOP-REAL 2); ( p `2 > 0 implies for x, a being Real
for r being positive Real st 0 <= a & a < (+ (x,r)) . p holds
ex r1 being positive Real st
( r1 <= p `2 & Ball (p,r1) c= (+ (x,r)) " ].a,1.] ) )
assume A1:
p `2 > 0
; for x, a being Real
for r being positive Real st 0 <= a & a < (+ (x,r)) . p holds
ex r1 being positive Real st
( r1 <= p `2 & Ball (p,r1) c= (+ (x,r)) " ].a,1.] )
let x, a be Real; for r being positive Real st 0 <= a & a < (+ (x,r)) . p holds
ex r1 being positive Real st
( r1 <= p `2 & Ball (p,r1) c= (+ (x,r)) " ].a,1.] )
let r be positive Real; ( 0 <= a & a < (+ (x,r)) . p implies ex r1 being positive Real st
( r1 <= p `2 & Ball (p,r1) c= (+ (x,r)) " ].a,1.] ) )
set f = + (x,r);
assume that
A2:
0 <= a
and
A3:
a < (+ (x,r)) . p
; ex r1 being positive Real st
( r1 <= p `2 & Ball (p,r1) c= (+ (x,r)) " ].a,1.] )
A4:
p = |[(p `1),(p `2)]|
by EUCLID:53;
then
p in the carrier of Niemytzki-plane
by A1, Lm1;
then
(+ (x,r)) . p in the carrier of I[01]
by FUNCT_2:5;
then
(+ (x,r)) . p <= 1
by BORSUK_1:40, XXREAL_1:1;
then A5:
a < 1
by A3, XXREAL_0:2;
per cases
( a = 0 or a > 0 )
by A2;
suppose A6:
a = 0
;
ex r1 being positive Real st
( r1 <= p `2 & Ball (p,r1) c= (+ (x,r)) " ].a,1.] )reconsider r1 =
p `2 as
positive Real by A1;
reconsider A =
Ball (
p,
r1) as
Subset of
Niemytzki-plane by A4, Lm1, Th20;
take
r1
;
( r1 <= p `2 & Ball (p,r1) c= (+ (x,r)) " ].a,1.] )thus
r1 <= p `2
;
Ball (p,r1) c= (+ (x,r)) " ].a,1.]let u be
object ;
TARSKI:def 3 ( not u in Ball (p,r1) or u in (+ (x,r)) " ].a,1.] )assume A7:
u in Ball (
p,
r1)
;
u in (+ (x,r)) " ].a,1.]then reconsider q =
u as
Point of
(TOP-REAL 2) ;
A8:
q = |[(q `1),(q `2)]|
by EUCLID:53;
q in A
by A7;
then A9:
q `2 >= 0
by A8, Lm1, Th18;
q in A
by A7;
then reconsider z =
q as
Element of
Niemytzki-plane ;
A10:
(+ (x,r)) . z >= 0
by BORSUK_1:40, XXREAL_1:1;
y=0-line misses Ball (
p,
r1)
by A4, Th21;
then
not
q in y=0-line
by A7, XBOOLE_0:3;
then A11:
q `2 <> 0
by A8;
A12:
(+ (x,r)) . z <= 1
by BORSUK_1:40, XXREAL_1:1;
|[x,0]| `2 = 0
by EUCLID:52;
then
(+ (x,r)) . q <> 0
by A11, A9, Th60;
then
(+ (x,r)) . z in ].a,1.]
by A10, A12, A6, XXREAL_1:2;
hence
u in (+ (x,r)) " ].a,1.]
by FUNCT_2:38;
verum end; suppose
a > 0
;
ex r1 being positive Real st
( r1 <= p `2 & Ball (p,r1) c= (+ (x,r)) " ].a,1.] )then reconsider b =
a as
positive Real ;
set r1 =
min (
(|.(p - |[x,(r * a)]|).| - (r * a)),
(p `2));
A13:
(
min (
(|.(p - |[x,(r * a)]|).| - (r * a)),
(p `2))
= |.(p - |[x,(r * a)]|).| - (r * a) or
min (
(|.(p - |[x,(r * a)]|).| - (r * a)),
(p `2))
= p `2 )
by XXREAL_0:def 9;
A14:
b <> (+ (x,r)) . p
by A3;
not
|.(p - |[x,(r * a)]|).| < r * a
by A3, A5, Th63;
then
|.(p - |[x,(r * a)]|).| > r * a
by A14, A1, A5, Th62, XXREAL_0:1;
then reconsider r1 =
min (
(|.(p - |[x,(r * a)]|).| - (r * a)),
(p `2)) as
positive Real by A13, A1, XREAL_1:50;
take
r1
;
( r1 <= p `2 & Ball (p,r1) c= (+ (x,r)) " ].a,1.] )thus
r1 <= p `2
by XXREAL_0:17;
Ball (p,r1) c= (+ (x,r)) " ].a,1.]then reconsider A =
Ball (
p,
r1) as
Subset of
Niemytzki-plane by A4, Lm1, Th20;
let u be
object ;
TARSKI:def 3 ( not u in Ball (p,r1) or u in (+ (x,r)) " ].a,1.] )assume A15:
u in Ball (
p,
r1)
;
u in (+ (x,r)) " ].a,1.]then reconsider q =
u as
Point of
(TOP-REAL 2) ;
u in A
by A15;
then reconsider z =
q as
Point of
Niemytzki-plane ;
A16:
q = |[(q `1),(q `2)]|
by EUCLID:53;
q in A
by A15;
then A17:
q `2 >= 0
by A16, Lm1, Th18;
A18:
now (+ (x,r)) . z > a
|.(p - |[x,(r * a)]|).| - (r * a) >= r1
by XXREAL_0:17;
then A19:
(r * a) + r1 <= (|.(p - |[x,(r * a)]|).| - (r * a)) + (r * a)
by XREAL_1:6;
assume
not
(+ (x,r)) . z > a
;
contradictionthen
|.(q - |[x,(r * a)]|).| <= r * a
by A2, A5, A17, Th64;
then A20:
|.(|[x,(r * a)]| - q).| <= r * a
by TOPRNS_1:27;
A21:
|.(|[x,(r * a)]| - q).| + |.(q - p).| >= |.(|[x,(r * a)]| - p).|
by TOPRNS_1:34;
|.(q - p).| < r1
by A15, TOPREAL9:7;
then
|.(|[x,(r * a)]| - q).| + |.(q - p).| < (r * a) + r1
by A20, XREAL_1:8;
then
|.(|[x,(r * a)]| - p).| < (r * a) + r1
by A21, XXREAL_0:2;
hence
contradiction
by A19, TOPRNS_1:27;
verum end;
(+ (x,r)) . z <= 1
by BORSUK_1:40, XXREAL_1:1;
then
(+ (x,r)) . z in ].a,1.]
by A18, XXREAL_1:2;
hence
u in (+ (x,r)) " ].a,1.]
by FUNCT_2:38;
verum end;