let x be real number ; :: thesis: for a, r being real positive number holds Ball |[x,(r * a)]|,(r * a) c= (+ x,r) " ].0 ,a.[
let a, r be real positive number ; :: thesis: Ball |[x,(r * a)]|,(r * a) c= (+ x,r) " ].0 ,a.[
let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in Ball |[x,(r * a)]|,(r * a) or u in (+ x,r) " ].0 ,a.[ )
assume A1: u in Ball |[x,(r * a)]|,(r * a) ; :: thesis: u in (+ x,r) " ].0 ,a.[
then reconsider p = u as Point of (TOP-REAL 2) ;
Ball |[x,(r * a)]|,(r * a) c= y>=0-plane by Th24;
then reconsider q = p as Point of Niemytzki-plane by A1, Def3;
A2: ( q = |[(p `1 ),(p `2 )]| & (+ x,r) . q in the carrier of I[01] ) by EUCLID:57, FUNCT_2:7;
then A3: ( (+ x,r) . q <= 1 & (+ x,r) . q >= 0 & p `2 >= 0 ) by Lm1, Th22, BORSUK_1:83, XXREAL_1:1;

A4: now

assume (+ x,r) . p = 0 ; :: thesis: contradiction
then p = |[x,0 ]| by A3, Th64;
then ( p in y=0-line & Ball |[x,(r * a)]|,(r * a) misses y=0-line ) by Th19, Th25;
hence contradiction by A1, XBOOLE_0:3; :: thesis: verum

end;

per cases ( a > 1 or a <= 1 ) ;

suppose a > 1 ; :: thesis: u in (+ x,r) " ].0 ,a.[

then ( (+ x,r) . q < a & (+ x,r) . q > 0 ) by A3, A4, XXREAL_0:2;
then (+ x,r) . q in ].0 ,a.[ by XXREAL_1:4;
hence u in (+ x,r) " ].0 ,a.[ by FUNCT_2:46; :: thesis: verum

end;

suppose A5: a <= 1 ; :: thesis: u in (+ x,r) " ].0 ,a.[

|.(p - |[x,(r * a)]|).| < r * a by A1, TOPREAL9:7;
then ( (+ x,r) . p < a & (+ x,r) . q > 0 ) by A2, A4, A5, Th67, BORSUK_1:83, XXREAL_1:1;
then (+ x,r) . q in ].0 ,a.[ by XXREAL_1:4;
hence u in (+ x,r) " ].0 ,a.[ by FUNCT_2:46; :: thesis: verum

end;

end;