let x be Real; :: thesis: for a, r being positive Real holds (Ball (|[x,(r * a)]|,(r * a))) \/ {|[x,0]|} c= (+ (x,r)) " [.0,a.[
let a, r be positive Real; :: thesis: (Ball (|[x,(r * a)]|,(r * a))) \/ {|[x,0]|} c= (+ (x,r)) " [.0,a.[
let u be object ; :: 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;
A3: |[x,0]| in y>=0-plane ;
Ball (|[x,(r * a)]|,(r * a)) c= y>=0-plane by Th20;
then reconsider q = p as Point of Niemytzki-plane by A3, A2, Lm1, TARSKI:def 1;
A4: (+ (x,r)) . q <= 1 by BORSUK_1:40, XXREAL_1:1;
A5: (+ (x,r)) . q >= 0 by BORSUK_1:40, 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 A4, XXREAL_0:2;
then (+ (x,r)) . q in [.0,a.[ by A5, XXREAL_1:3;
hence u in (+ (x,r)) " [.0,a.[ by FUNCT_2:38; :: thesis: verum

end;

suppose A6: ( 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 A6, Th63;
then (+ (x,r)) . q in [.0,a.[ by A5, XXREAL_1:3;
hence u in (+ (x,r)) " [.0,a.[ by FUNCT_2:38; :: 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:38; :: thesis: verum

end;

end;