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

per cases ( a > 1 or ( a <= 1 & u in Ball |[x,(r * a)]|,(r * a) ) or u = |[x,0 ]| ) by A2, TARSKI:def 1;

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

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

end;

suppose A4: ( a <= 1 & u in Ball |[x,(r * a)]|,(r * a) ) ; :: thesis: u in (+ x,r) " [.0 ,a.[

then |.(p - |[x,(r * a)]|).| < r * a by TOPREAL9:7;
then (+ x,r) . p < a by A4, Th67;
then (+ x,r) . q in [.0 ,a.[ by A3, XXREAL_1:3;
hence u in (+ x,r) " [.0 ,a.[ by FUNCT_2:46; :: thesis: verum

end;

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

then (+ x,r) . u = 0 by Def5;
then (+ x,r) . q in [.0 ,a.[ by XXREAL_1:3;
hence u in (+ x,r) " [.0 ,a.[ by FUNCT_2:46; :: thesis: verum

end;

end;