let x be Real; :: thesis: for a, r being positive Real holds Ball (|[x,(r * a)]|,(r * a)) c= (+ (x,r)) " ].0,a.[
let a, r be positive Real; :: thesis: Ball (|[x,(r * a)]|,(r * a)) c= (+ (x,r)) " ].0,a.[
let u be object ; :: 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 Th20;
then reconsider q = p as Point of Niemytzki-plane by A1, Def3;
q = |[(p `1),(p `2)]| by EUCLID:53;
then A2: p `2 >= 0 by Lm1, Th18;
A3: now :: thesis: not (+ (x,r)) . p = 0
assume (+ (x,r)) . p = 0 ; :: thesis: contradiction
then p = |[x,0]| by A2, Th60;
then A4: p in y=0-line ;
Ball (|[x,(r * a)]|,(r * a)) misses y=0-line by Th21;
hence contradiction by A4, A1, XBOOLE_0:3; :: thesis: verum
end;
A5: (+ (x,r)) . q <= 1 by BORSUK_1:40, XXREAL_1:1;
per cases ( a > 1 or a <= 1 ) ;
suppose A6: a > 1 ; :: thesis: u in (+ (x,r)) " ].0,a.[
A7: (+ (x,r)) . q > 0 by A3, BORSUK_1:40, XXREAL_1:1;
(+ (x,r)) . q < a by A6, A5, XXREAL_0:2;
then (+ (x,r)) . q in ].0,a.[ by A7, XXREAL_1:4;
hence u in (+ (x,r)) " ].0,a.[ by FUNCT_2:38; :: thesis: verum
end;
suppose A8: a <= 1 ; :: thesis: u in (+ (x,r)) " ].0,a.[
|.(p - |[x,(r * a)]|).| < r * a by A1, TOPREAL9:7;
then A9: (+ (x,r)) . p < a by A8, Th63;
(+ (x,r)) . q > 0 by A3, BORSUK_1:40, XXREAL_1:1;
then (+ (x,r)) . q in ].0,a.[ by A9, XXREAL_1:4;
hence u in (+ (x,r)) " ].0,a.[ by FUNCT_2:38; :: thesis: verum
end;
end;