let p be Point of (TOP-REAL 2); :: thesis: ( p `2 > 0 implies for x, a being real number
for r being real positive number st 0 <= a & a < (+ x,r) . p holds
ex r1 being real positive number st
( r1 <= p `2 & Ball p,r1 c= (+ x,r) " ].a,1.] ) )
assume A1:
p `2 > 0
; :: thesis: for x, a being real number
for r being real positive number st 0 <= a & a < (+ x,r) . p holds
ex r1 being real positive number st
( r1 <= p `2 & Ball p,r1 c= (+ x,r) " ].a,1.] )
let x, a be real number ; :: thesis: for r being real positive number st 0 <= a & a < (+ x,r) . p holds
ex r1 being real positive number st
( r1 <= p `2 & Ball p,r1 c= (+ x,r) " ].a,1.] )
let r be real positive number ; :: thesis: ( 0 <= a & a < (+ x,r) . p implies ex r1 being real positive number st
( r1 <= p `2 & Ball p,r1 c= (+ x,r) " ].a,1.] ) )
set f = + x,r;
assume A2:
( 0 <= a & a < (+ x,r) . p )
; :: thesis: ex r1 being real positive number st
( r1 <= p `2 & Ball p,r1 c= (+ x,r) " ].a,1.] )
A3:
p = |[(p `1 ),(p `2 )]|
by EUCLID:57;
then
p in the carrier of Niemytzki-plane
by A1, Lm1;
then
(+ x,r) . p in the carrier of I[01]
by FUNCT_2:7;
then
(+ x,r) . p <= 1
by BORSUK_1:83, XXREAL_1:1;
then A4:
a < 1
by A2, XXREAL_0:2;
per cases
( a = 0 or a > 0 )
by A2;
suppose A5:
a = 0
;
:: thesis: ex r1 being real positive number st
( r1 <= p `2 & Ball p,r1 c= (+ x,r) " ].a,1.] )reconsider r1 =
p `2 as
real positive number by A1;
take
r1
;
:: thesis: ( r1 <= p `2 & Ball p,r1 c= (+ x,r) " ].a,1.] )thus
r1 <= p `2
;
:: thesis: Ball p,r1 c= (+ x,r) " ].a,1.]reconsider A =
Ball p,
r1 as
Subset of
Niemytzki-plane by A3, Lm1, Th24;
let u be
set ;
:: according to TARSKI:def 3 :: thesis: ( not u in Ball p,r1 or u in (+ x,r) " ].a,1.] )assume A6:
u in Ball p,
r1
;
:: thesis: u in (+ x,r) " ].a,1.]then reconsider q =
u as
Point of
(TOP-REAL 2) ;
q in A
by A6;
then reconsider z =
q as
Element of
Niemytzki-plane ;
y=0-line misses Ball p,
r1
by A3, Th25;
then
( not
q in y=0-line &
q = |[(q `1 ),(q `2 )]| &
q in A )
by A6, EUCLID:57, XBOOLE_0:3;
then
(
q `2 <> 0 &
|[x,0 ]| `2 = 0 &
q `2 >= 0 &
(+ x,r) . z in the
carrier of
I[01] )
by Lm1, Th22, EUCLID:56, FUNCT_2:7;
then
(
(+ x,r) . q <> 0 &
(+ x,r) . z >= 0 &
(+ x,r) . z <= 1 )
by Th64, BORSUK_1:83, XXREAL_1:1;
then
(+ x,r) . z in ].a,1.]
by A5, XXREAL_1:2;
hence
u in (+ x,r) " ].a,1.]
by FUNCT_2:46;
:: thesis: verum end; suppose
a > 0
;
:: thesis: ex r1 being real positive number st
( r1 <= p `2 & Ball p,r1 c= (+ x,r) " ].a,1.] )then reconsider b =
a as
real positive number ;
set r1 =
min (|.(p - |[x,(r * a)]|).| - (r * a)),
(p `2 );
( not
a > (+ x,r) . p &
b <> (+ x,r) . p )
by A2;
then
( not
|.(p - |[x,(r * a)]|).| < r * a &
|.(p - |[x,(r * a)]|).| <> r * a )
by A1, A4, Th66, Th67;
then A7:
|.(p - |[x,(r * a)]|).| > r * a
by XXREAL_0:1;
(
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;
then reconsider r1 =
min (|.(p - |[x,(r * a)]|).| - (r * a)),
(p `2 ) as
real positive number by A1, A7, XREAL_1:52;
take
r1
;
:: thesis: ( r1 <= p `2 & Ball p,r1 c= (+ x,r) " ].a,1.] )thus
r1 <= p `2
by XXREAL_0:17;
:: thesis: Ball p,r1 c= (+ x,r) " ].a,1.]then reconsider A =
Ball p,
r1 as
Subset of
Niemytzki-plane by A3, Lm1, Th24;
let u be
set ;
:: according to TARSKI:def 3 :: thesis: ( not u in Ball p,r1 or u in (+ x,r) " ].a,1.] )assume A8:
u in Ball p,
r1
;
:: thesis: u in (+ x,r) " ].a,1.]then reconsider q =
u as
Point of
(TOP-REAL 2) ;
u in A
by A8;
then reconsider z =
q as
Point of
Niemytzki-plane ;
(
q = |[(q `1 ),(q `2 )]| &
q in A )
by A8, EUCLID:57;
then A9:
q `2 >= 0
by Lm1, Th22;
A10:
now assume
not
(+ x,r) . z > a
;
:: thesis: contradictionthen
|.(q - |[x,(r * a)]|).| <= r * a
by A2, A4, A9, Th68;
then
(
|.(|[x,(r * a)]| - q).| <= r * a &
|.(q - p).| < r1 )
by A8, TOPREAL9:7, TOPRNS_1:28;
then
(
|.(|[x,(r * a)]| - q).| + |.(q - p).| >= |.(|[x,(r * a)]| - p).| &
|.(p - |[x,(r * a)]|).| - (r * a) >= r1 &
|.(|[x,(r * a)]| - q).| + |.(q - p).| < (r * a) + r1 )
by TOPRNS_1:35, XREAL_1:10, XXREAL_0:17;
then
(
|.(|[x,(r * a)]| - p).| < (r * a) + r1 &
(r * a) + r1 <= (|.(p - |[x,(r * a)]|).| - (r * a)) + (r * a) &
|.(|[x,(r * a)]| - p).| = |.(p - |[x,(r * a)]|).| )
by TOPRNS_1:28, XREAL_1:8, XXREAL_0:2;
hence
contradiction
;
:: thesis: verum end;
(+ x,r) . z in the
carrier of
I[01]
by FUNCT_2:7;
then
(+ x,r) . z <= 1
by BORSUK_1:83, XXREAL_1:1;
then
(+ x,r) . z in ].a,1.]
by A10, XXREAL_1:2;
hence
u in (+ x,r) " ].a,1.]
by FUNCT_2:46;
:: thesis: verum end;